English
Let α be a preorder and β a linear-ordered semilattice. If f and g are antitone on a set s, then the function x ↦ max{f(x), g(x)} is antitone on s.
Русский
Пусть α — предобразное множество, β — линейно упорядоченная полузамкнутая. Если f,g антимонотонны на s, то x ↦ max{f(x), g(x)} антимонотонна на s.
LaTeX
$$$\forall x,y\in s:\ x\le y\Rightarrow \max\{f(x),g(x)\}\ge \max\{f(y),g(y)\}$$$
Lean4
/-- Pointwise maximum of two antitone functions is an antitone function. -/
protected theorem max [Preorder α] [LinearOrder β] {f g : α → β} {s : Set α} (hf : AntitoneOn f s)
(hg : AntitoneOn g s) : AntitoneOn (fun x => max (f x) (g x)) s :=
hf.sup hg
