He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo en el que se comentan 9 pruebas en Lean de la propiedad
Las subsucesiones de las sucesiones convergentes tienen el mismo límite que la sucesión.
usando los estilos aplicativo, funcional y declarativo.
A continuación, se muestra el vídeo
y el código de la teoría utilizada
import data.real.basic variable {u : ℕ → ℝ} variables {a : ℝ} variable {φ : ℕ → ℕ} -- ---------------------------------------------------- -- Nota. Usaremos los siguientes conceptos estudiados -- anteriormente. -- ---------------------------------------------------- notation `|`x`|` := abs x def limite : (ℕ → ℝ) → ℝ → Prop := λ u c, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| ≤ ε def extraccion : (ℕ → ℕ) → Prop | φ := ∀ n m, n < m → φ n < φ m lemma id_mne_extraccion (h : extraccion φ) : ∀ n, n ≤ φ n := begin intros n, induction n with m HI, { linarith }, { exact nat.succ_le_of_lt (by linarith [h m (m+1) (by linarith)]) }, end lemma extraccion_mye (h : extraccion φ) : ∀ N N', ∃ n ≥ N', φ n ≥ N := λ N N', ⟨max N N', le_max_right N N', le_trans (le_max_left N N') (id_mne_extraccion h (max N N'))⟩ -- ---------------------------------------------------- -- Ejercicio. Demostrar que las subsucesiones de las -- sucesiones convergentes tienen el mismo límite que -- la sucesión. -- ---------------------------------------------------- -- 1ª demostración example (h : limite u a) (hφ : extraccion φ) : limite (u ∘ φ) a := begin -- unfold limite, intros ε hε, -- unfold limite at h, cases h ε hε with N hN, use N, intros n hn, apply hN, apply le_trans hn, exact id_mne_extraccion hφ n, end -- 2ª demostración example (h : limite u a) (hφ : extraccion φ) : limite (u ∘ φ) a := begin intros ε hε, cases h ε hε with N hN, use N, intros n hn, apply hN, exact le_trans hn (id_mne_extraccion hφ n), end -- 3ª demostración example (h : limite u a) (hφ : extraccion φ) : limite (u ∘ φ) a := begin intros ε hε, cases h ε hε with N hN, use N, intros n hn, exact hN (φ n) (le_trans hn (id_mne_extraccion hφ n)), end -- 4ª demostración example (h : limite u a) (hφ : extraccion φ) : limite (u ∘ φ) a := begin intros ε hε, cases h ε hε with N hN, use N, exact λ n hn, hN (φ n) (le_trans hn (id_mne_extraccion hφ n)), end -- 5ª demostración example (h : limite u a) (hφ : extraccion φ) : limite (u ∘ φ) a := begin intros ε hε, -- unfold limite at h, cases h ε hε with N hN, exact ⟨N, λ n hn, hN (φ n) (le_trans hn (id_mne_extraccion hφ n))⟩, end -- 6ª demostración example (h : limite u a) (hφ : extraccion φ) : limite (u ∘ φ) a := begin intros ε hε, exact (exists.elim (h ε hε) (λ N hN, ⟨N, λ n hn, hN (φ n) (le_trans hn (id_mne_extraccion hφ n))⟩)), end -- 7ª demostración example (h : limite u a) (hφ : extraccion φ) : limite (u ∘ φ) a := λ ε hε, (exists.elim (h ε hε) (λ N hN, ⟨N, λ n hn, hN (φ n) (le_trans hn (id_mne_extraccion hφ n))⟩)) -- 8ª demostración example (h : limite u a) (hφ : extraccion φ) : limite (u ∘ φ) a := begin intros ε hε, unfold limite at h, cases h ε hε with N hN, use N, intros n hn, apply hN, calc N ≤ n : hn ... ≤ φ n : id_mne_extraccion hφ n, end -- 9ª demostración example (h : limite u a) (hφ : extraccion φ) : limite (u ∘ φ) a := assume ε, assume hε : ε > 0, exists.elim (h ε hε) ( assume N, assume hN : ∀ n, n ≥ N → |u n - a| ≤ ε, have h1 : ∀n, n ≥ N → |(u ∘ φ) n - a| ≤ ε, { assume n, assume hn : n ≥ N, have h2 : N ≤ φ n, from calc N ≤ n : hn ... ≤ φ n : id_mne_extraccion hφ n, show |(u ∘ φ) n - a| ≤ ε, from hN (φ n) h2, }, show ∃ N, ∀n, n ≥ N → |(u ∘ φ) n - a| ≤ ε, from exists.intro N h1) |