English
Every lattice-ordered commutative group is a distributive lattice; i.e., the lattice operations satisfy the distributive law.
Русский
Любая решётка-упорядоченная коммутативная группа является распределяемой решёткой: выполняются законы распределения ∧ и ∨.
LaTeX
$$$ \forall x,y,z:\ x \wedge (y \vee z) = (x \wedge y) \vee (x \wedge z) \\ and \\ (x \vee y) \wedge z = (x \wedge z) \vee (y \wedge z) $$$
Lean4
/-- Every lattice ordered commutative group is a distributive lattice. -/
-- Non-comm case needs cancellation law https://ncatlab.org/nlab/show/distributive+lattice
@[to_additive /-- Every lattice ordered commutative additive group is a distributive lattice -/
]
def toDistribLattice (α : Type*) [Lattice α] [CommGroup α] [MulLeftMono α] : DistribLattice α where
le_sup_inf x y
z := by
rw [← mul_le_mul_iff_left (x ⊓ (y ⊓ z)), inf_mul_sup x (y ⊓ z), ← inv_mul_le_iff_le_mul, le_inf_iff]
constructor
· rw [inv_mul_le_iff_le_mul, ← inf_mul_sup x y]
exact mul_le_mul' (inf_le_inf_left _ inf_le_left) inf_le_left
· rw [inv_mul_le_iff_le_mul, ← inf_mul_sup x z]
exact mul_le_mul' (inf_le_inf_left _ inf_le_right) inf_le_right
