English
Let α be a type equipped with a binary infimum operation that makes it a SemilatticeInf, and fix elements a ≤ b in α. Then the closed interval Icc(a,b) = { x ∈ α | a ≤ x ≤ b } inherits a SemilatticeInf structure from α via the inherited order; in particular, the infimum in Icc(a,b) is obtained by taking the infimum in α and verifying it lies again in [a,b].
Русский
Пусть α — множество с операцией наименьшего элементов (поле полупорядочения) и возьмем элементы a ≤ b. Тогда замкнутый интервал Icc(a,b) = { x ∈ α | a ≤ x ≤ b } наследует структуру SemilatticeInf от α по унаследованному порядку; особенно наименьшее в Icc(a,b) получается как наименьшее в α и принадлежит [a,b].
LaTeX
$$$\text{If } [\text{SemilatticeInf } \alpha], \ a \le b, \text{ then }\ \text{Icc}(a,b) \text{ with the induced order is a } \operatorname{SemilatticeInf}. $$$
Lean4
instance semilatticeInf [SemilatticeInf α] : SemilatticeInf (Icc a b) :=
Subtype.semilatticeInf fun _ _ hx hy => ⟨le_inf hx.1 hy.1, le_trans inf_le_left hx.2⟩
