English
If β has a SemilatticeSup, then the space of order-preserving maps α →o β also has a SemilatticeSup, defined pointwise by (f ⊔ g)(a) = f(a) ⊔ g(a).
Русский
Если β имеет семилаттиевлуп, то множество отображений сохраняющих порядок α →o β также имеет SemilatticeSup, заданный по точкам: (f ⊔ g)(a) = f(a) ⊔ g(a).
LaTeX
$$$[SemilatticeSup\; \beta] \Rightarrow [SemilatticeSup\; (\alpha \to_o \beta)]$ with $(f ⊔ g)(a) = f(a) ⊔ g(a).$$$
Lean4
instance [SemilatticeSup β] : SemilatticeSup (α →o β) :=
{ (_ : PartialOrder (α →o β)) with
sup := Max.max
le_sup_left := fun _ _ _ => le_sup_left
le_sup_right := fun _ _ _ => le_sup_right
sup_le := fun _ _ _ h₀ h₁ x => sup_le (h₀ x) (h₁ x) }
