English
If f and g are monotone functions from α to β, where α has a preorder and β is a semilattice with join, then the function x ↦ max(f(x), g(x)) is monotone.
Русский
Если f и g — монотонные отображения α → β, где α имеет предorder, а β — полная решётка с операцией объединения, то функция x ↦ max(f(x), g(x)) монотонна.
LaTeX
$$$ \text{Monotone}(f) \rightarrow \text{Monotone}(g) \rightarrow \text{Monotone}(x \mapsto \max(f(x), g(x))) $$$
Lean4
/-- Pointwise supremum of two monotone functions is a monotone function. -/
protected theorem sup [Preorder α] [SemilatticeSup β] {f g : α → β} (hf : Monotone f) (hg : Monotone g) :
Monotone (f ⊔ g) := fun _ _ h => sup_le_sup (hf h) (hg h)
