English
Let f and g be functions with local maxima on s at a. If op: β × γ → δ is monotone in both arguments, then x ↦ op(f(x), g(x)) has a local maximum on s at a.
Русский
Пусть f и g имеют локальные максимумы на s в точке a. Если op: β × γ → δ монотонна по обоим аргументам, то x ↦ op(f(x), g(x)) имеет локальный максимум на s в a.
LaTeX
$$$\\IsLocalMaxOn\\ f\\ s\\ a \\land \\IsLocalMaxOn\\ g\\ s\\ a \\land \\bigl(\\forall b_1,b_2\\in \\beta,\\ b_1 \\le b_2 \\Rightarrow \\forall c_1,c_2\\in \\gamma,\\ c_1 \\le c_2 \\Rightarrow \\operatorname{op}(b_1,c_1) \\le \\operatorname{op}(b_2,c_2)\\bigr) \\Rightarrow \\IsLocalMaxOn (x \\mapsto \\operatorname{op}(f(x))(g(x)))\\ s\\ a$$
Lean4
nonrec theorem bicomp_mono [Preorder δ] {op : β → γ → δ} (hop : ((· ≤ ·) ⇒ (· ≤ ·) ⇒ (· ≤ ·)) op op)
(hf : IsLocalMaxOn f s a) {g : α → γ} (hg : IsLocalMaxOn g s a) : IsLocalMaxOn (fun x => op (f x) (g x)) s a :=
hf.bicomp_mono hop hg
