En los retículos, una distributiva del ínfimo implica la otra
Demostrar con Lean4 que si α es un retículo tal que se
$$(∀ x, y, z) [x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z))]$$
entonces
$$(a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c)$$
para todos los elementos de α.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Order.Lattice variable {α : Type _} [Lattice α] variable (a b c : α) example (h : ∀ x y z : α, x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z)) : (a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c) := by sorry |
Demostración en lenguaje natural
Se demuestra por la siguiente cadena de igualdades
\begin{align}
(a ⊔ b) ⊓ c &= c ⊓ (a ⊔ b) &&\text{[por conmutatividad de ⊓]} \\
&= (c ⊓ a) ⊔ (c ⊓ b) &&\text{[por la hipótesis]} \\
&= (a ⊓ c) ⊔ (c ⊓ b) &&\text{[por conmutatividad de ⊓]} \\
&= (a ⊓ c) ⊔ (b ⊓ c) &&\text{[por conmutatividad de ⊓]}
\end{align}
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 |
import Mathlib.Order.Lattice variable {α : Type _} [Lattice α] variable (a b c : α) -- 1ª demostración example (h : ∀ x y z : α, x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z)) : (a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c) := calc (a ⊔ b) ⊓ c = c ⊓ (a ⊔ b) := by rw [inf_comm] _ = (c ⊓ a) ⊔ (c ⊓ b) := by rw [h] _ = (a ⊓ c) ⊔ (c ⊓ b) := by rw [@inf_comm _ _ c a] _ = (a ⊓ c) ⊔ (b ⊓ c) := by rw [@inf_comm _ _ c b] -- 2ª demostración example (h : ∀ x y z : α, x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z)) : (a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c) := by simp [h, inf_comm] -- Lemas usados -- ============ -- #check (inf_comm : a ⊓ b = b ⊓ a) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 22.
