La sucesión constante sₙ = c converge a c
En Lean, una sucesión \(s₀, s₁, s₂, …\) se puede representar mediante una función \(s : ℕ → ℝ\) de forma que \(s(n)\) es \(sₙ\).
Se define que a es el límite de la sucesión \(s\), por
|
1 2 |
def limite (s : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε |
Demostrar que el límite de la sucesión constante \(sₙ = c\) es \(c\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Real.Basic def limite (s : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε example : limite (fun _ : ℕ ↦ c) c := by sorry |
1. Demostración en lenguaje natural
Tenemos que demostrar que para cada \(ε ∈ ℝ\) tal que \(ε > 0\), existe un \(N ∈ ℕ\), tal que \((∀n ∈ ℕ)[n ≥ N → |s(n) – a| < ε]\). Basta tomar \(N\) como \(0\), ya que para todo \(n ≥ N\) se tiene
\begin{align}
|s(n) – a| &= |a – a| \\
&= |0| \\
&= 0 \\
&< ε \\
\end{align}
2. Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 |
import Mathlib.Data.Real.Basic def limite (s : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε -- 1ª demostración -- =============== example : limite (fun _ : ℕ ↦ c) c := by intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |(fun _ => c) n - c| < ε use 0 -- ⊢ ∀ (n : ℕ), n ≥ 0 → |(fun _ => c) n - c| < ε intros n _hn -- n : ℕ -- hn : n ≥ 0 -- ⊢ |(fun _ => c) n - c| < ε show |(fun _ => c) n - c| < ε calc |(fun _ => c) n - c| = |c - c| := by dsimp _ = |0| := by {congr ; exact sub_self c} _ = 0 := abs_zero _ < ε := hε -- 2ª demostración -- =============== example : limite (fun _ : ℕ ↦ c) c := by intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |(fun _ => c) n - c| < ε use 0 -- ⊢ ∀ (n : ℕ), n ≥ 0 → |(fun _ => c) n - c| < ε intros n _hn -- n : ℕ -- hn : n ≥ 0 -- ⊢ |(fun _ => c) n - c| < ε show |(fun _ => c) n - c| < ε calc |(fun _ => c) n - c| = 0 := by simp _ < ε := hε -- 3ª demostración -- =============== example : limite (fun _ : ℕ ↦ c) c := by intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |(fun _ => c) n - c| < ε aesop -- 4ª demostración -- =============== example : limite (fun _ : ℕ ↦ c) c := by intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |(fun _ => c) n - c| < ε aesop -- 5ª demostración -- =============== example : limite (fun _ : ℕ ↦ c) c := fun ε hε ↦ by aesop -- Lemas usados -- ============ -- #check (sub_self a : a - a = 0) |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
3. Demostraciones con Isabelle/HOL
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 |
theory Limite_de_sucesiones_constantes imports Main HOL.Real begin definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where "limite u c ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - c¦ < ε)" (* 1ª demostración *) lemma "limite (λ n. c) c" proof (unfold limite_def) show "∀ε>0. ∃k::nat. ∀n≥k. ¦c - c¦ < ε" proof (intro allI impI) fix ε :: real assume "0 < ε" have "∀n≥0::nat. ¦c - c¦ < ε" proof (intro allI impI) fix n :: nat assume "0 ≤ n" have "c - c = 0" by (simp only: diff_self) then have "¦c - c¦ = 0" by (simp only: abs_eq_0_iff) also have "… < ε" by (simp only: ‹0 < ε›) finally show "¦c - c¦ < ε" by this qed then show "∃k::nat. ∀n≥k. ¦c - c¦ < ε" by (rule exI) qed qed (* 2ª demostración *) lemma "limite (λ n. c) c" proof (unfold limite_def) show "∀ε>0. ∃k::nat. ∀n≥k. ¦c - c¦ < ε" proof (intro allI impI) fix ε :: real assume "0 < ε" have "∀n≥0::nat. ¦c - c¦ < ε" by (simp add: ‹0 < ε›) then show "∃k::nat. ∀n≥k. ¦c - c¦ < ε" by (rule exI) qed qed (* 3ª demostración *) lemma "limite (λ n. c) c" unfolding limite_def by simp (* 4ª demostración *) lemma "limite (λ n. c) c" by (simp add: limite_def) end |
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 41.
