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