instDistribLattice — Mathlib

English

If α and β are distributive lattices, then α × β is a distributive lattice, with distributive law holding coordinatewise.

Русский

Если α и β — распределительные решётки, то α × β — распределительная решётка, и закон распределения выполняется координатно.

LaTeX

$$[(a,b) ∧ ((c,d) ∨ (e,f))] = [((a,b) ∧ (c,d)) ∨ ((a,b) ∧ (e,f))]coordinatewise$$

Lean4

instance instDistribLattice [DistribLattice α] [DistribLattice β] : DistribLattice (α × β) where
  le_sup_inf _ _ _ := ⟨le_sup_inf, le_sup_inf⟩

Похожие утверждения