Los límites son menores o iguales que las cotas superiores
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 a es una cota superior de u por
1 2 |
def cota_superior (u : ℕ → ℝ) (a : ℝ) := ∀ n, u n ≤ a |
Demostrar que si x es el límite de la sucesión u e y es una cota superior de u, entonces x ≤ y.
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 |
import data.real.basic variable (u : ℕ → ℝ) variables (x y : ℝ) notation `|`x`|` := abs x def limite (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| < ε def cota_superior (u : ℕ → ℝ) (a : ℝ) := ∀ n, u n ≤ a example (hx : limite u x) (hy : cota_superior u y) : x ≤ y := 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 |
import data.real.basic variable (u : ℕ → ℝ) variables (x y : ℝ) notation `|`x`|` := abs x def limite (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| < ε def cota_superior (u : ℕ → ℝ) (a : ℝ) := ∀ n, u n ≤ a lemma aux : (∀ ε > 0, y ≤ x + ε) → y ≤ x := begin contrapose!, intro h, use (y-x)/2, split ; linarith, end -- 1º demostración example (hx : limite u x) (hy : cota_superior u y) : x ≤ y := begin apply aux, intros ε hε, cases hx ε hε with k hk, specialize hk k rfl.ge, replace hk : -ε < u k - x := neg_lt_of_abs_lt hk, replace hk : x < u k + ε := neg_lt_sub_iff_lt_add'.mp hk, apply le_of_lt, exact lt_add_of_lt_add_right hk (hy k), end -- 2º demostración example (hx : limite u x) (hy : cota_superior u y) : x ≤ y := begin apply aux, intros ε hε, cases hx ε hε with k hk, specialize hk k rfl.ge, apply le_of_lt, calc x < u k + ε : neg_lt_sub_iff_lt_add'.mp (neg_lt_of_abs_lt hk) ... ≤ y + ε : add_le_add_right (hy k) ε, end -- 3º demostración example (hx : limite u x) (hy : cota_superior u y) : x ≤ y := begin apply aux, intros ε hε, cases hx ε hε with k hk, specialize hk k (by linarith), rw abs_lt at hk, linarith [hy k], 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 |
theory Los_limites_son_menores_o_iguales_que_las_cotas_superiores imports Main HOL.Real begin definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where "limite u c ⟷ (∀ε>0. ∃k. ∀n≥k. ¦u n - c¦ < ε)" definition cota_superior :: "(nat ⇒ real) ⇒ real ⇒ bool" where "cota_superior u c ⟷ (∀n. u n ≤ c)" (* 1ª demostración *) lemma fixes x y :: real assumes "limite u x" "cota_superior u y" shows "x ≤ y" proof (rule field_le_epsilon) fix ε :: real assume "0 < ε" then obtain k where hk : "∀n≥k. ¦u n - x¦ < ε" using assms(1) limite_def by auto then have "¦u k - x¦ < ε" by simp then have "-ε < u k - x" by simp then have "x < u k + ε" by simp moreover have "u k ≤ y" using assms(2) cota_superior_def by simp ultimately show "x ≤ y + ε" by simp qed (* 2ª demostración *) lemma fixes x y :: real assumes "limite u x" "cota_superior u y" shows "x ≤ y" proof (rule field_le_epsilon) fix ε :: real assume "0 < ε" then obtain k where hk : "∀n≥k. ¦u n - x¦ < ε" using assms(1) limite_def by auto then have "x < u k + ε" by auto moreover have "u k ≤ y" using assms(2) cota_superior_def by simp ultimately show "x ≤ y + ε" by simp qed (* 3ª demostración *) lemma fixes x y :: real assumes "limite u x" "cota_superior u y" shows "x ≤ y" proof (rule field_le_epsilon) fix ε :: real assume "0 < ε" then obtain k where hk : "∀n≥k. ¦u n - x¦ < ε" using assms(1) limite_def by auto then show "x ≤ y + ε" using assms(2) cota_superior_def by (smt (verit) order_refl) 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]