English
Pointwise supremum of two monotone functions is monotone on a set.
Русский
Порядковый верхний предел по каждоик функции на множестве сохраняется для двух монотонных функций.
LaTeX
$$$ [Preorder α] [SemilatticeSup β] {f g : α → β} {s : Set α} (hf : MonotoneOn f s) (hg : MonotoneOn g s) : MonotoneOn (f \sqcup g) s$$$
Lean4
/-- Pointwise supremum of two monotone functions is a monotone function. -/
protected theorem sup [Preorder α] [SemilatticeSup β] {f g : α → β} {s : Set α} (hf : MonotoneOn f s)
(hg : MonotoneOn g s) : MonotoneOn (f ⊔ g) s := fun _ hx _ hy h => sup_le_sup (hf hx hy h) (hg hx hy h)
