Límite de sucesiones constantes
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
1 2 |
def limite : (ℕ → ℝ) → ℝ → Prop := λ u a, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - a| < ε |
donde se usa la notación |x| para el valor absoluto de x
1 |
notation `|`x`|` := abs x |
Demostrar que el límite de la sucesión constante c es c.
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 7 8 9 10 11 12 13 |
import data.real.basic variable (u : ℕ → ℝ) variable (c : ℝ) notation `|`x`|` := abs x def limite : (ℕ → ℝ) → ℝ → Prop := λ u a, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - a| < ε example : limite (λ n, c) c := sorry |
[expand title=»Soluciones con Lean»]
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 78 79 80 81 82 83 84 85 |
import data.real.basic variable (u : ℕ → ℝ) variable (c : ℝ) notation `|`x`|` := abs x def limite : (ℕ → ℝ) → ℝ → Prop := λ u a, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - a| < ε -- 1ª demostración -- =============== example : limite (λ n, c) c := begin unfold limite, intros ε hε, use 0, intros n hn, dsimp, simp, exact hε, end -- 2ª demostración -- =============== example : limite (λ n, c) c := begin intros ε hε, use 0, rintro n -, norm_num, assumption, end -- 3ª demostración -- =============== example : limite (λ n, c) c := begin intros ε hε, use 0, intros n hn, calc |(λ n, c) n - c| = |c - c| : rfl ... = 0 : by simp ... < ε : hε end -- 4ª demostración -- =============== example : limite (λ n, c) c := begin intros ε hε, by finish, end -- 5ª demostración -- =============== example : limite (λ n, c) c := λ ε hε, by finish -- 6ª demostración -- =============== example : limite (λ n, c) c := assume ε, assume hε : ε > 0, exists.intro 0 ( assume n, assume hn : n ≥ 0, show |(λ n, c) n - c| < ε, from calc |(λ n, c) n - c| = |c - c| : rfl ... = 0 : by simp ... < ε : hε) |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]
[expand title=»Soluciones 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 59 60 61 62 63 64 65 66 67 68 69 |
(* --------------------------------------------------------------------- -- En Isabelle/HOL, 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 -- definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" -- where "limite u c ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - c¦ < ε)" -- -- Demostrar que el límite de la sucesión constante c es c. -- ------------------------------------------------------------------ *) 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 |
En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]