Las sucesiones acotadas por cero son nulas
Demostrar que las sucesiones acotadas por cero son nulas.
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 7 8 9 10 11 |
import data.real.basic import tactic variable (u : ℕ → ℝ) notation `|`x`|` := abs x example (h : ∀ n, |u n| ≤ 0) : ∀ n, u n = 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 |
import data.real.basic import tactic variable (u : ℕ → ℝ) notation `|`x`|` := abs x -- 1ª demostración example (h : ∀ n, |u n| ≤ 0) : ∀ n, u n = 0 := begin intro n, rw ← abs_eq_zero, specialize h n, apply le_antisymm, { exact h, }, { exact abs_nonneg (u n), }, end -- 2ª demostración example (h : ∀ n, |u n| ≤ 0) : ∀ n, u n = 0 := begin intro n, rw ← abs_eq_zero, specialize h n, exact le_antisymm h (abs_nonneg (u n)), end -- 3ª demostración example (h : ∀ n, |u n| ≤ 0) : ∀ n, u n = 0 := begin intro n, rw ← abs_eq_zero, exact le_antisymm (h n) (abs_nonneg (u n)), end -- 4ª demostración example (h : ∀ n, |u n| ≤ 0) : ∀ n, u n = 0 := begin intro n, exact abs_eq_zero.mp (le_antisymm (h n) (abs_nonneg (u n))), end -- 5ª demostración example (h : ∀ n, |u n| ≤ 0) : ∀ n, u n = 0 := λ n, abs_eq_zero.mp (le_antisymm (h n) (abs_nonneg (u n))) -- 6ª demostración example (h : ∀ n, |u n| ≤ 0) : ∀ n, u n = 0 := by finish |
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 |
theory Las_sucesiones_acotadas_por_cero_son_nulas imports Main HOL.Real begin (* 1ª demostración *) lemma fixes a :: "nat ⇒ real" assumes "∀n. ¦a n¦ ≤ 0" shows "∀n. a n = 0" proof (rule allI) fix n have "¦a n¦ = 0" proof (rule antisym) show "¦a n¦ ≤ 0" using assms by (rule allE) next show " 0 ≤ ¦a n¦" by (rule abs_ge_zero) qed then show "a n = 0" by (simp only: abs_eq_0_iff) qed (* 2ª demostración *) lemma fixes a :: "nat ⇒ real" assumes "∀n. ¦a n¦ ≤ 0" shows "∀n. a n = 0" proof (rule allI) fix n have "¦a n¦ = 0" proof (rule antisym) show "¦a n¦ ≤ 0" try using assms by (rule allE) next show " 0 ≤ ¦a n¦" by simp qed then show "a n = 0" by simp qed (* 3ª demostración *) lemma fixes a :: "nat ⇒ real" assumes "∀n. ¦a n¦ ≤ 0" shows "∀n. a n = 0" proof (rule allI) fix n have "¦a n¦ = 0" using assms by auto then show "a n = 0" by simp qed (* 4ª demostración *) lemma fixes a :: "nat ⇒ real" assumes "∀n. ¦a n¦ ≤ 0" shows "∀n. a n = 0" using assms by auto 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]