He añadido a la lista Lógica con Lean el vídeo Teorema del emparedado en el que se comentan pruebas en Lean del teorema del emparedado:
Si dos sucesiones tienen el mismo límite, entonces las sucesiones que están comprendidas entre éstas también tienen el mismo límite.
A continuación, se muestra el vídeo
import data.real.basic variables (u v w : ℕ → ℝ) variable (a : ℝ) -- ---------------------------------------------------- -- Ejercicio 1. Definir la notación |x| para el valor -- absoluto de x. -- ---------------------------------------------------- notation `|`x`|` := abs x -- ---------------------------------------------------- -- Ejercicio 2. Definir la función -- limite : (ℕ → ℝ) → ℝ → Prop -- tal que (limite u c) expresa que c es el límite de -- la sucesión u. -- ---------------------------------------------------- def limite : (ℕ → ℝ) → ℝ → Prop := λ u c, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| ≤ ε -- ---------------------------------------------------- -- Ejercicio 3. Demostrar que si dos sucesiones tienen -- el mismo límite, entonces las sucesiones que están -- comprendidas entre éstas también tienen el mismo -- límite. -- ---------------------------------------------------- -- Nota. En la demostración se usará el siguiente lema: lemma max_ge_iff {p q r : ℕ} : r ≥ max p q ↔ r ≥ p ∧ r ≥ q := max_le_iff -- 1ª demostración -- =============== example (hu : limite u a) (hw : limite w a) (h : ∀ n, u n ≤ v n) (h' : ∀ n, v n ≤ w n) : limite v a := begin intros ε hε, cases hu ε hε with N hN, clear hu, cases hw ε hε with N' hN', clear hw hε, use max N N', intros n hn, rw max_ge_iff at hn, specialize hN n hn.1, specialize hN' n hn.2, specialize h n, specialize h' n, clear hn, rw abs_le at *, split, { calc -ε ≤ u n - a : hN.1 ... ≤ v n - a : by linarith, }, { calc v n - a ≤ w n - a : by linarith ... ≤ ε : hN'.2, }, end -- 2ª demostración example (hu : limite u a) (hw : limite w a) (h : ∀ n, u n ≤ v n) (h' : ∀ n, v n ≤ w n) : limite v a := begin intros ε hε, cases hu ε hε with N hN, clear hu, cases hw ε hε with N' hN', clear hw hε, use max N N', intros n hn, rw max_ge_iff at hn, specialize hN n (by linarith), specialize hN' n (by linarith), specialize h n, specialize h' n, rw abs_le at *, split, { linarith, }, { linarith, }, end -- 3ª demostración example (hu : limite u a) (hw : limite w a) (h : ∀ n, u n ≤ v n) (h' : ∀ n, v n ≤ w n) : limite v a := begin intros ε hε, cases hu ε hε with N hN, clear hu, cases hw ε hε with N' hN', clear hw hε, use max N N', intros n hn, rw max_ge_iff at hn, specialize hN n (by linarith), specialize hN' n (by linarith), specialize h n, specialize h' n, rw abs_le at *, split ; linarith, end -- 4ª demostración example (hu : limite u a) (hw : limite w a) (h : ∀ n, u n ≤ v n) (h' : ∀ n, v n ≤ w n) : limite v a := assume ε, assume hε : ε > 0, exists.elim (hu ε hε) ( assume N, assume hN : ∀ (n : ℕ), n ≥ N → |u n - a| ≤ ε, exists.elim (hw ε hε) ( assume N', assume hN' : ∀ (n : ℕ), n ≥ N' → |w n - a| ≤ ε, show ∃ N, ∀ n, n ≥ N → |v n - a| ≤ ε, from exists.intro (max N N') ( assume n, assume hn : n ≥ max N N', have h1 : n ≥ N ∧ n ≥ N', from max_ge_iff.mp hn, have h2 : -ε ≤ v n - a, { have h2a : |u n - a| ≤ ε, from hN n h1.1, calc -ε ≤ u n - a : and.left (abs_le.mp h2a) ... ≤ v n - a : by linarith [h n], }, have h3 : v n - a ≤ ε, { have h3a : |w n - a| ≤ ε, from hN' n h1.2, calc v n - a ≤ w n - a : by linarith [h' n] ... ≤ ε : and.right (abs_le.mp h3a), }, show |v n - a| ≤ ε, from abs_le.mpr (and.intro h2 h3)))) |