ForMatUS: Si |x| < ε, para todo ε > 0, entonces x = 0
He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo en el que se comentan 10 pruebas en Lean de la propiedad
Si |x| < ε, para todo ε > 0, entonces x = 0
usando los estilos declarativos, aplicativos y funcional.
A continuación, se muestra el vídeo
|
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 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 |
import data.real.basic variable (x : ℝ) -- ---------------------------------------------------- -- Ejercicio 1. Definir la notación |x| para el valor -- absoluto de x. -- ---------------------------------------------------- notation `|`x`|` := abs x -- ---------------------------------------------------- -- Ejercicio 2. Demostrar que si |x| < ε, para todo -- ε > 0, entonces x = 0 -- ---------------------------------------------------- -- 1ª demostración example (h : ∀ ε > 0, |x| < ε) : x = 0 := begin rw ← abs_eq_zero, apply eq_of_le_of_forall_le_of_dense, { exact abs_nonneg x, }, { intros ε hε, apply le_of_lt, exact h ε hε, }, end -- 2ª demostración example (h : ∀ ε > 0, |x| < ε) : x = 0 := begin rw ← abs_eq_zero, apply eq_of_le_of_forall_le_of_dense, { exact abs_nonneg x, }, { intros ε hε, exact le_of_lt (h ε hε), }, end -- 3ª demostración example (h : ∀ ε > 0, |x| < ε) : x = 0 := begin rw ← abs_eq_zero, apply eq_of_le_of_forall_le_of_dense, { exact abs_nonneg x, }, { exact λ ε hε, le_of_lt (h ε hε), }, end -- 4ª demostración example (h : ∀ ε > 0, |x| < ε) : x = 0 := begin rw ← abs_eq_zero, apply eq_of_le_of_forall_le_of_dense (abs_nonneg x) (λ ε hε, le_of_lt (h ε hε)), end -- 5ª demostración example (h : ∀ ε > 0, |x| < ε) : x = 0 := abs_eq_zero.mp (eq_of_le_of_forall_le_of_dense (abs_nonneg x) (λ ε hε, le_of_lt (h ε hε))) -- 6ª demostración example (h : ∀ ε > 0, |x| < ε) : x = 0 := have h1 : 0 ≤ |x|, from abs_nonneg x, have h2 : ∀ ε, ε > 0 → |x| ≤ ε, { assume ε, assume hε : ε > 0, have h2a : |x| < ε, from h ε hε, show |x| ≤ ε, from le_of_lt h2a }, have h3 : |x| = 0, from eq_of_le_of_forall_le_of_dense h1 h2, show x = 0, from abs_eq_zero.mp h3 -- 7ª demostración example (h : ∀ ε > 0, |x| < ε) : x = 0 := have h1 : 0 ≤ |x|, from abs_nonneg x, have h2 : ∀ ε, ε > 0 → |x| ≤ ε, { assume ε, assume hε : ε > 0, have h2a : |x| < ε, from h ε hε, show |x| ≤ ε, from le_of_lt h2a }, have h3 : |x| = 0, from eq_of_le_of_forall_le_of_dense h1 h2, abs_eq_zero.mp h3 -- 8ª demostración example (h : ∀ ε > 0, |x| < ε) : x = 0 := have h1 : 0 ≤ |x|, from abs_nonneg x, have h2 : ∀ ε, ε > 0 → |x| ≤ ε, { assume ε, assume hε : ε > 0, have h2a : |x| < ε, from h ε hε, show |x| ≤ ε, from le_of_lt h2a }, abs_eq_zero.mp (eq_of_le_of_forall_le_of_dense h1 h2) -- 9ª demostración example (h : ∀ ε > 0, |x| < ε) : x = 0 := have h1 : 0 ≤ |x|, from abs_nonneg x, have h2 : ∀ ε, ε > 0 → |x| ≤ ε, { assume ε, assume hε : ε > 0, show |x| ≤ ε, from le_of_lt (h ε hε) }, abs_eq_zero.mp (eq_of_le_of_forall_le_of_dense h1 h2) -- 10ª demostración example (h : ∀ ε > 0, |x| < ε) : x = 0 := abs_eq_zero.mp (eq_of_le_of_forall_le_of_dense (abs_nonneg x) (λ ε hε, le_of_lt (h ε hε))) |