distribLattice — Mathlib

English

If α is a distributive lattice, then Ici a is a distributive lattice under the inherited order.

Русский

Если α — распределительная решётка, то Ici a также является распределительной решёткой.

LaTeX

$$$$\\text{DistribLattice}(\\mathrm{Ici}(a)).$$$$

Lean4

instance distribLattice [DistribLattice α] {a : α} : DistribLattice (Ici a) :=
  { Ici.lattice with le_sup_inf := fun _ _ _ => le_sup_inf }

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