lattice — Mathlib

English

If α is a lattice, then Icc(a,b) is a lattice under the inherited order, formed from the semilatticeInf and semilatticeSup structures on Icc.

Русский

Если α — решетка, то Icc(a,b) образует решётку по унаследованному порядку, используя соответствующие операции inf и sup.

LaTeX

$$$\text{If } [\text{Lattice } \alpha], \ Icc(a,b) \text{ is a lattice with inherited inf and sup.}$$$

Lean4

instance lattice [Lattice α] : Lattice (Icc a b) :=
  { Icc.semilatticeInf, Icc.semilatticeSup with }

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