Menu Close

En los retículos, una distributiva del supremo implica la otra

José A. Alonso

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:

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

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

Escribe un comentario