El límite de uₙ es a syss el de uₙ-a es 0

Demostrar con Lean4 que el límite de u es a si, y sólo si, el de ua es 0.

Para ello, completar la siguiente teoría de Lean4:

1. Demostración en lenguaje natural

Se prueba por la siguiente cadena de equivalencias
el límite de u es a(ε>0)(N)(nN)[|u(n)a|<ε](ε>0)(N)(nN)[|(u(n)a)0|<ε]el límite de ua es 0

2. Demostraciones con Lean4

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

3. Demostraciones con Isabelle/HOL

Escribe un comentario