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 }