instLattice — Mathlib

English

If α is a lattice, then WithZero α is a lattice, with the join and meet defined by lifting α's infimum and supremum to WithZero and including 0 as the bottom element.

Русский

Пусть α — решётка. Тогда WithZero α является решёткой, в которой операции наибольшего и наименьшего поднимаются из α, при этом 0 служит нулём-головой.

LaTeX

$$$\mathrm{Lattice}(\alpha) \rightarrow \mathrm{Lattice}(\mathrm{WithZero}\,\alpha)$$$

Lean4

instance instLattice [Lattice α] : Lattice (WithZero α) :=
  { WithZero.semilatticeSup, WithZero.semilatticeInf with }

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