Teorema del emparedado

Demostrar con Lean4 el teorema del emparedado.

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

1. Demostración en lenguaje natural

Tenemos que demostrar que para cada \(ε > 0\), existe un \(N ∈ ℕ\) tal que
\[ (∀ n ≥ N)[|v(n) – a| ≤ ε] \tag{1} \]

Puesto que el límite de \(u\) es \(a\), existe un \(U ∈ ℕ\) tal que
\[ (∀ n ≥ U)[|u(n) – a| ≤ ε] \tag{2} \]
y, puesto que el límite de \(w\) es \(a\), existe un \(W ∈ ℕ\) tal que
\[ (∀ n ≥ W)[|w(n) – a| ≤ ε] \tag{3} \]
Sea \(N = \text{máx}(U, W)\). Veamos que se verifica (1). Para ello, sea \(n ≥ N\). Entonces, \(n ≥ U\), \(n ≥ W\) y, por (2) y (3), se tiene que
\begin{align}
|u(n) – a| &≤ ε \tag{4} \\
|w(n) – a| &≤ ε \tag{5}
\end{align}
Para demostrar que
\[ |v(n) – a| ≤ ε \]
basta demostrar las siguientes desigualdades
\begin{align}
-ε ≤ &v(n) – a \tag{6} \\
&v(n) – a ≤ ε \tag{7}
\end{align}
La demostración de (6) es
\begin{align}
-ε &≤ u(n) – a &&\text{[por (4)]} \\
&≤ v(n) – a &&\text{[por hipótesis]}
\end{align}
La demostración de (7) es
\begin{align}
v(n) – a &≤ w(n) – a &&\text{[por hipótesis]} \\
&≤ ε &&\text{[por (5)]}
\end{align}

2. Demostraciones con Lean4

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

3. Demostraciones con Isabelle/HOL

Escribe un comentario