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 |
Read More «En los retículos, una distributiva del supremo implica la otra»