English
If α is a SemilatticeSup, then the closed interval Icc(a,b) inherits a SemilatticeSup structure from α via the inherited order, with the supremum on Icc given by the supremum in α.
Русский
Если начальный множитель α образует SemilatticeSup, то замкнутый интервал Icc(a,b) наследует структуру SemilatticeSup от α по унаследованному порядку; верхняя граница в Icc задаётся через верхнюю границу в α.
LaTeX
$$$\text{If } [\text{SemilatticeSup } \alpha], \ a \le b, \text{ then }\ \text{Icc}(a,b) \text{ is a SemilatticeSup with } x \vee y \text{ defined pointwise.}$$$
Lean4
instance semilatticeSup [SemilatticeSup α] : SemilatticeSup (Icc a b) :=
Subtype.semilatticeSup fun _ _ hx hy => ⟨le_trans hx.1 le_sup_left, sup_le hx.2 hy.2⟩
