lattice — Mathlib

English

PartENat carries a lattice structure with meet given by minimum and join by maximum under the order ≤.

Русский

PartENat имеет структуру решетки: наименьшее и наибольшее задают минимум и максимум относительно порядка ≤.

LaTeX

$$$ \text{Lattice}(\mathrm{PartENat}) $$$

Lean4

noncomputable instance lattice : Lattice PartENat :=
  { PartENat.semilatticeSup with
    inf := min
    inf_le_left := min_le_left
    inf_le_right := min_le_right
    le_inf := fun _ _ _ => le_min }

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