English
Let f: α → β and g: α → γ be functions, and s ⊆ α. If a ∈ s maximizes f on s and also maximizes g on s, and op: β → γ → δ is monotone in both arguments (i.e., nondecreasing in each argument with respect to ≤), then the pointwise combination h(x) = op(f(x), g(x)) attains a maximum on s at a.
Русский
Пусть f: α → β и g: α → γ, s ⊆ α. Если a ∈ s максимизирует f на s и максимизирует g на s, и op: β → γ → δ неубывает по каждому аргументу, то h(x) = op(f(x), g(x)) достигает максимума на s в точке a.
LaTeX
$$$hop \land IsMaxOn f s a \land IsMaxOn g s a \Rightarrow IsMaxOn (\lambda x. op (f x) (g x)) s a$$$
Lean4
theorem bicomp_mono [Preorder δ] {op : β → γ → δ} (hop : ((· ≤ ·) ⇒ (· ≤ ·) ⇒ (· ≤ ·)) op op) (hf : IsMaxOn f s a)
{g : α → γ} (hg : IsMaxOn g s a) : IsMaxOn (fun x => op (f x) (g x)) s a :=
IsMaxFilter.bicomp_mono hop hf hg
