Pruebas en Lean de “Si |x – y| ≤ ε, para todo ε > 0, entonces x = y”
He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo en el que se comentan pruebas en Lean de la propiedad:
Si |x – y| ≤ ε, para todo ε > 0, entonces x = y
usando los estilos declarativos, aplicativos, funcional y automático.
A continuación, se muestra el vídeo
y el código de la teoría utilizada
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 |
import data.real.basic variables (x y : ℝ) -- ---------------------------------------------------- -- Ejercicio 1. Definir la notación |x| para el valor -- absoluto de x. -- ---------------------------------------------------- notation `|`x`|` := abs x -- ---------------------------------------------------- -- Ejercicio 2. Demostrar que si |x - y| ≤ ε, para todo -- ε > 0, entonces x = y. -- ---------------------------------------------------- -- Se usará el lema demostrado anteriormente lemma cero_de_abs_mne_todos (h : ∀ ε > 0, |x| ≤ ε) : x = 0 := abs_eq_zero.mp (eq_of_le_of_forall_le_of_dense (abs_nonneg x) h) -- 1ª demostración example (h : ∀ ε > 0, |x - y| ≤ ε) : x = y := begin rw ← sub_eq_zero, exact cero_de_abs_mne_todos (x - y) h, end -- 2ª demostración lemma ig_de_abs_sub_mne_todos (h : ∀ ε > 0, |x - y| ≤ ε) : x = y := sub_eq_zero.mp (cero_de_abs_mne_todos (x - y) h) |