Si f es continua en a y el límite de u(n) es a, entonces el límite de f(u(n)) es f(a)
En Lean, se puede definir que a es el límite de la sucesión u por
1 2 |
def limite (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| < ε |
y que f es continua en a por
1 2 |
def continua_en_punto (f : ℝ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ δ > 0, ∀ x, |x - a| ≤ δ → |f x - f a| ≤ ε |
Demostrar que si f es continua en a y el límite de uₙ es a, entonces el límite de f(uₙ) es f(a).
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 |
import data.real.basic variable {f : ℝ → ℝ} variable {a : ℝ} variable {u : ℕ → ℝ} notation `|`x`|` := abs x def limite (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| ≤ ε def continua_en_punto (f : ℝ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ δ > 0, ∀ x, |x - a| ≤ δ → |f x - f a| ≤ ε example (hf : continua_en_punto f a) (hu : limite u a) : limite (f ∘ u) (f a) := 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 |
import data.real.basic variable {f : ℝ → ℝ} variable {a : ℝ} variable {u : ℕ → ℝ} notation `|`x`|` := abs x def limite (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| ≤ ε def continua_en_punto (f : ℝ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ δ > 0, ∀ x, |x - a| ≤ δ → |f x - f a| ≤ ε -- 1ª demostración example (hf : continua_en_punto f a) (hu : limite u a) : limite (f ∘ u) (f a) := begin intros ε hε, rcases hf ε hε with ⟨δ, hδ1, hδ2⟩, cases hu δ hδ1 with k hk, use k, intros n hn, apply hδ2, exact hk n hn, end -- 2ª demostración example (hf : continua_en_punto f a) (hu : limite u a) : limite (f ∘ u) (f a) := begin intros ε hε, rcases hf ε hε with ⟨δ, hδ1, hδ2⟩, cases hu δ hδ1 with k hk, exact ⟨k, λ n hn, hδ2 (u n) (hk n hn)⟩, end -- 3ª demostración example (hf : continua_en_punto f a) (hu : limite u a) : limite (f ∘ u) (f a) := begin intros ε hε, obtain ⟨δ, hδ1, hδ2⟩ := hf ε hε, obtain ⟨k, hk⟩ := hu δ hδ1, exact ⟨k, λ n hn, hδ2 (u n) (hk n hn)⟩, 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 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 86 87 88 89 90 91 92 93 94 95 96 97 98 99 |
theory CS_de_continuidad imports Main HOL.Real begin definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where "limite u c ⟷ (∀ε>0. ∃k. ∀n≥k. ¦u n - c¦ ≤ ε)" definition continua_en_punto :: "(real ⇒ real) ⇒ real ⇒ bool" where "continua_en_punto f a ⟷ (∀ε>0. ∃δ>0. ∀x. ¦x - a¦ ≤ δ ⟶ ¦f x - f a¦ ≤ ε)" (* 1ª demostración *) lemma assumes "continua_en_punto f a" "limite u a" shows "limite (f ∘ u) (f a)" proof (unfold limite_def; intro allI impI) fix ε :: real assume "0 < ε" then obtain δ where hδ1 : "δ > 0" and hδ2 :" (∀x. ¦x - a¦ ≤ δ ⟶ ¦f x - f a¦ ≤ ε)" using assms(1) continua_en_punto_def by auto obtain k where hk : "∀n≥k. ¦u n - a¦ ≤ δ" using assms(2) limite_def hδ1 by auto have "∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε" proof (intro allI impI) fix n assume "n ≥ k" then have "¦u n - a¦ ≤ δ" using hk by auto then show "¦(f ∘ u) n - f a¦ ≤ ε" using hδ2 by simp qed then show "∃k. ∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε" by auto qed (* 2ª demostración *) lemma assumes "continua_en_punto f a" "limite u a" shows "limite (f ∘ u) (f a)" proof (unfold limite_def; intro allI impI) fix ε :: real assume "0 < ε" then obtain δ where hδ1 : "δ > 0" and hδ2 :" (∀x. ¦x - a¦ ≤ δ ⟶ ¦f x - f a¦ ≤ ε)" using assms(1) continua_en_punto_def by auto obtain k where hk : "∀n≥k. ¦u n - a¦ ≤ δ" using assms(2) limite_def hδ1 by auto have "∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε" using hk hδ2 by simp then show "∃k. ∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε" by auto qed (* 3ª demostración *) lemma assumes "continua_en_punto f a" "limite u a" shows "limite (f ∘ u) (f a)" proof (unfold limite_def; intro allI impI) fix ε :: real assume "0 < ε" then obtain δ where hδ1 : "δ > 0" and hδ2 :" (∀x. ¦x - a¦ ≤ δ ⟶ ¦f x - f a¦ ≤ ε)" using assms(1) continua_en_punto_def by auto obtain k where hk : "∀n≥k. ¦u n - a¦ ≤ δ" using assms(2) limite_def hδ1 by auto then show "∃k. ∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε" using hk hδ2 by auto qed (* 4ª demostración *) lemma assumes "continua_en_punto f a" "limite u a" shows "limite (f ∘ u) (f a)" proof (unfold limite_def; intro allI impI) fix ε :: real assume "0 < ε" then obtain δ where hδ : "δ > 0 ∧ (∀x. ¦x - a¦ ≤ δ ⟶ ¦f x - f a¦ ≤ ε)" using assms(1) continua_en_punto_def by auto then obtain k where "∀n≥k. ¦u n - a¦ ≤ δ" using assms(2) limite_def by auto then show "∃k. ∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε" using hδ by auto qed (* 5ª demostración *) lemma assumes "continua_en_punto f a" "limite u a" shows "limite (f ∘ u) (f a)" using assms continua_en_punto_def limite_def by force 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]