Unicidad del límite de las sucesiones convergentes

En Lean, una sucesión \(u₀, u₁, u₂, …\) se puede representar mediante una función \((u : ℕ → ℝ)\) de forma que \(u(n)\) es \(uₙ\).

Se define que \(a\) es el límite de la sucesión \(u\), por

Demostrar con Lean4 que cada sucesión tiene como máximo un límite.

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

1. Demostración en lenguaje natural

Tenemos que demostrar que si \(u\) es una sucesión y \(a\) y \(b\) son límites de \(u\), entonces \(a = b\). Para ello, basta demostrar que \(a ≤ b\) y \(b ≤ a\).

Demostraremos que \(b ≤ a\) por reducción al absurdo. Supongamos que \(b ≰ a\). Sea \(ε = b – a\). Entonces, ε/2 > 0 y, puesto que \(a\) es un límite de \(u\), existe un \(A ∈ ℕ\) tal que
\[ (∀n ∈ ℕ)\left[n ≥ A → |u(n) – a| < \frac{ε}{2}\right] \tag{1} \]
y, puesto que \(b\) también es un límite de \(u\), existe un \(B ∈ ℕ\) tal que
\[ (∀n ∈ ℕ)\left[n ≥ B → |u(n) – b| < \frac{ε}{2}\right] \tag{2} \]
Sea \(N = máx(A, B)\). Entonces, \(N ≥ A\) y \(N ≥ B\) y, por (2) y (3), se tiene
\begin{align}
|u(N) – a| &< \frac{ε}{2} \tag{3} \\
|u(N) – b| &< \frac{ε}{2} \tag{4}
\end{align}
Para obtener una contradicción basta probar que \(ε < ε\). Su prueba es
\begin{align}
ε &= b – a \\
&= |b – a| \\
&= |(b – a) + (u(N) – u(N))| \\
&= |(u(N) – a) + (b – u(N))| \\
&≤ |u(N) – a| + |b – u(N)| \\
&= |u(N) – a| + |u(N) – b| \\
&< \frac{ε}{2} + \frac{ε}{2} && \text{[por (3) y (4)]} \\
&= ε
\end{align}

La demostración de \(a ≤ b\) es análoga a la anterior.

2. Demostraciones con Lean4

Demostraciones interactivas

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

3. Demostraciones con Isabelle/HOL

Escribe un comentario