El límite de u(n) es a si y solo si el de u(n)-a es 0
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 u(n) es a si y solo si el de u(n)-a es 0.
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
import data.real.basic import tactic variable {u : ℕ → ℝ} variables {a c x : ℝ} notation `|`x`|` := abs x def limite : (ℕ → ℝ) → ℝ → Prop := λ u c, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε example : limite u a ↔ limite (λ i, u i - a) 0 := 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 |
import data.real.basic import tactic variable {u : ℕ → ℝ} variables {a c x : ℝ} notation `|`x`|` := abs x def limite : (ℕ → ℝ) → ℝ → Prop := λ u c, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε -- 1ª demostración -- =============== example : limite u a ↔ limite (λ i, u i - a) 0 := begin split, { intros h ε hε, convert h ε hε, norm_num, }, { intros h ε hε, convert h ε hε, norm_num, }, end -- 2ª demostración -- =============== example : limite u a ↔ limite (λ i, u i - a) 0 := begin split; { intros h ε hε, convert h ε hε, norm_num, }, end -- 3ª demostración -- =============== lemma limite_con_suma (c : ℝ) (h : limite u a) : limite (λ i, u i + c) (a + c) := λ ε hε, (by convert h ε hε; norm_num) lemma CNS_limite_con_suma (c : ℝ) : limite u a ↔ limite (λ i, u i + c) (a + c) := begin split, { apply limite_con_suma }, { intro h, convert limite_con_suma (-c) h; simp, }, end example (u : ℕ → ℝ) (a : ℝ) : limite u a ↔ limite (λ i, u i - a) 0 := begin convert CNS_limite_con_suma (-a), simp, end |
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 |
theory "El_limite_de_u_es_a_syss_el_de_u-a_es_0" 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 u a ⟷ limite (λ i. u i - a) 0" proof - have "limite u a ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - a¦ < ε)" by (rule limite_def) also have "… ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦(u n - a) - 0¦ < ε)" by simp also have "… ⟷ limite (λ i. u i - a) 0" by (rule limite_def[symmetric]) finally show "limite u a ⟷ limite (λ i. u i - a) 0" by this qed (* 2ª demostración *) lemma "limite u a ⟷ limite (λ i. u i - a) 0" proof - have "limite u a ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - a¦ < ε)" by (simp only: limite_def) also have "… ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦(u n - a) - 0¦ < ε)" by simp also have "… ⟷ limite (λ i. u i - a) 0" by (simp only: limite_def) finally show "limite u a ⟷ limite (λ i. u i - a) 0" by this qed (* 3ª demostración *) lemma "limite u a ⟷ limite (λ i. u i - a) 0" using limite_def by simp 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]