Demostrar con Lean4 que en los retículos se verifica que
\[ x ⊔ (x ⊓ y) = x \]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Order.Lattice variable {α : Type _} [Lattice α]-- variable (x y : α) example : x ⊔ (x ⊓ y) = x := by sorry |
Demostración en lenguaje natural
En la demostración se usarán los siguientes lemas
\begin{align}
&x ≤ y → y ≤ x → x = y \tag{L1} \\
&x ⊓ y ≤ x \tag{L2} \\
&x ≤ x \tag{L3} \\
&x ≤ x ⊔ y \tag{L4} \\
&x ≤ z → y ≤ z → x ⊔ y ≤ z \tag{L5}
\end{align}
Por L1, basta demostrar las siguientes relaciones:
\begin{align}
&x ⊔ (x ⊓ y) ≤ x \tag{1} \\
&x ≤ x ⊔ (x ⊓ y) &&\text{[que se tiene por L4]}
\end{align}
Para demostrar (1), por L5, basta probar las relaciones:
\begin{align}
&x ≤ x &&\text{[que se tiene por L3]} \\
&x ⊓ y ≤ x &&\text{[que se tiene por L2]}
\end{align}
Demostraciones con Lean4
import Mathlib.Order.Lattice variable {α : Type _} [Lattice α]-- variable (x y : α) -- 1ª demostración -- =============== example : x ⊔ (x ⊓ y) = x := by have h1 : x ⊔ (x ⊓ y) ≤ x { have h1a : x ≤ x := le_rfl have h1b : x ⊓ y ≤ x := inf_le_left show x ⊔ (x ⊓ y) ≤ x exact sup_le h1a h1b } have h2 : x ≤ x ⊔ (x ⊓ y) := le_sup_left show x ⊔ (x ⊓ y) = x exact le_antisymm h1 h2 -- 2ª demostración -- =============== example : x ⊔ (x ⊓ y) = x := by have h1 : x ⊔ (x ⊓ y) ≤ x := by simp have h2 : x ≤ x ⊔ (x ⊓ y) := by simp show x ⊔ (x ⊓ y) = x exact le_antisymm h1 h2 -- 3ª demostración -- =============== example : x ⊔ (x ⊓ y) = x := by apply le_antisymm . -- x ⊔ (x ⊓ y) ≤ x apply sup_le . -- x ≤ x apply le_rfl . -- x ⊓ y ≤ x apply inf_le_left . -- x ≤ x ⊔ (x ⊓ y) apply le_sup_left -- 4ª demostración -- =============== example : x ⊔ (x ⊓ y) = x := -- by apply? sup_inf_self -- 5ª demostración -- =============== example : x ⊔ (x ⊓ y) = x := by simp -- Lemas usados -- ============ -- variable (z : α) -- #check (le_rfl : x ≤ x) -- #check (inf_le_left : x ⊓ y ≤ x) -- #check (sup_le : x ≤ z → y ≤ z → x ⊔ y ≤ z) -- #check (le_sup_left : x ≤ x ⊔ y) -- #check (le_antisymm : x ≤ y → y ≤ x → x = y) -- #check (sup_inf_self : x ⊔ (x ⊓ y) = x) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 21.