Si ≤ es un preorden, entonces < es irreflexiva
Demostrar con Lean4 que si \(≤\) es un preorden, entonces \(<\) es irreflexiva.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Tactic variable {α : Type _} [Preorder α] variable (a : α) example : ¬a < a := by sorry |
Demostración en lenguaje natural
Se usará la siguiente propiedad de lo preórdenes
\[ (∀ a, b)[a < b ↔ a ≤ b ∧ b ≰ a] \]
Con dicha propiedad, lo que tenemos que demostrar se transforma en
\[ ¬(a ≤ a ∧ a ≰ a) \]
Para demostrarla, supongamos que
\[ a ≤ a ∧ a ≰ a \]
lo que es una contradicción.
Demostraciones con Lean4
|
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 |
import Mathlib.Tactic variable {α : Type _} [Preorder α] variable (a : α) -- 1ª demostración -- =============== example : ¬a < a := by rw [lt_iff_le_not_le] -- ⊢ ¬(a ≤ a ∧ ¬a ≤ a) rintro ⟨h1, h2⟩ -- h1 : a ≤ a -- h2 : ¬a ≤ a -- ⊢ False exact h2 h1 -- 2ª demostración -- =============== example : ¬a < a := irrefl a -- Lemas usados -- ============ -- variable (b : α) -- #check (lt_iff_le_not_le : a < b ↔ a ≤ b ∧ ¬b ≤ a) -- #check (irrefl a : ¬a < a) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 38.
