Unicidad del límite de las sucesiones convergentes
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 cada sucesión tiene como máximo un límite.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 |
import data.real.basic variables {u : ℕ → ℝ} variables {a b : ℝ} notation `|`x`|` := abs x def limite : (ℕ → ℝ) → ℝ → Prop := λ u c, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε example (ha : limite u a) (hb : limite u b) : a = b := 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 |
import data.real.basic variables {u : ℕ → ℝ} variables {a b : ℝ} notation `|`x`|` := abs x def limite : (ℕ → ℝ) → ℝ → Prop := λ u c, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε -- 1ª demostración -- =============== example (ha : limite u a) (hb : limite u b) : a = b := begin by_contra h, wlog hab : a < b, { have : a < b ∨ a = b ∨ b < a := lt_trichotomy a b, tauto }, set ε := b - a with hε, specialize ha (ε/2), have hε2 : ε/2 > 0 := by linarith, specialize ha hε2, cases ha with A hA, cases hb (ε/2) (by linarith) with B hB, set N := max A B with hN, have hAN : A ≤ N := le_max_left A B, have hBN : B ≤ N := le_max_right A B, specialize hA N hAN, specialize hB N hBN, rw abs_lt at hA hB, linarith, end -- 2ª demostración -- =============== example (ha : limite u a) (hb : limite u b) : a = b := begin by_contra h, wlog hab : a < b, { have : a < b ∨ a = b ∨ b < a := lt_trichotomy a b, tauto }, set ε := b - a with hε, cases ha (ε/2) (by linarith) with A hA, cases hb (ε/2) (by linarith) with B hB, set N := max A B with hN, have hAN : A ≤ N := le_max_left A B, have hBN : B ≤ N := le_max_right A B, specialize hA N hAN, specialize hB N hBN, rw abs_lt at hA hB, linarith, 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 46 47 |
theory Unicidad_del_limite_de_las_sucesiones_convergentes imports Main HOL.Real begin definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where "limite u c ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - c¦ < ε)" lemma aux : assumes "limite u a" "limite u b" shows "b ≤ a" proof (rule ccontr) assume "¬ b ≤ a" let ?ε = "b - a" have "0 < ?ε/2" using ‹¬ b ≤ a› by auto obtain A where hA : "∀n≥A. ¦u n - a¦ < ?ε/2" using assms(1) limite_def ‹0 < ?ε/2› by blast obtain B where hB : "∀n≥B. ¦u n - b¦ < ?ε/2" using assms(2) limite_def ‹0 < ?ε/2› by blast let ?C = "max A B" have hCa : "∀n≥?C. ¦u n - a¦ < ?ε/2" using hA by simp have hCb : "∀n≥?C. ¦u n - b¦ < ?ε/2" using hB by simp have "∀n≥?C. ¦a - b¦ < ?ε" proof (intro allI impI) fix n assume "n ≥ ?C" have "¦a - b¦ = ¦(a - u n) + (u n - b)¦" by simp also have "… ≤ ¦u n - a¦ + ¦u n - b¦" by simp finally show "¦a - b¦ < b - a" using hCa hCb ‹n ≥ ?C› by fastforce qed then show False by fastforce qed theorem assumes "limite u a" "limite u b" shows "a = b" proof (rule antisym) show "a ≤ b" using assms(2) assms(1) by (rule aux) next show "b ≤ a" using assms(1) assms(2) by (rule aux) qed 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]
