En los retículos, una distributiva del supremo implica la otra
Demostrar con Lean4 que si \(R\) es un retículo tal que
\[ (∀ x,\ y,\ z \in R) [x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z)] \]
entonces
\[ (a ⊓ b) ⊔ c = (a ⊔ c) ⊓ (b ⊔ c) \]
para todos los elementos del retículo.
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 la conmutatividad de ⊔]} \\
&= (c ⊔ a) ⊓ (c ⊔ b) &&\text{[por la hipótesis]} \\
&= (a ⊔ c) ⊓ (c ⊔ b) &&\text{[por la conmutatividad de ⊔]} \\
&= (a ⊔ c) ⊓ (b ⊔ c) &&\text{[por la 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 [sup_comm] _ = (c ⊔ a) ⊓ (c ⊔ b) := by rw [h] _ = (a ⊔ c) ⊓ (c ⊔ b) := by rw [@sup_comm _ _ c a] _ = (a ⊔ c) ⊓ (b ⊔ c) := by rw [@sup_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, sup_comm] -- Lemas usados -- ============ -- #check (sup_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.
