English
Let f and g be functions on a topological space, and let s be a subset with a ∈ s. If f has a local minimum on s at a and g has a local minimum on s at a, and if op: β × γ → δ is monotone in both arguments, then the pointwise combination x ↦ op(f(x), g(x)) has a local minimum on s at a.
Русский
Пусть f и g - функции на топологическом пространстве, пусть s - подмножество, и a ∈ s. Если f имеет локальный минимум на s в точке a и g имеет локальный минимум на s в точке a, и если op: β × γ → δ монотонна по каждому аргументу, то поочередная функция x ↦ op(f(x), g(x)) имеет локальный минимум на s в точке a.
LaTeX
$$$\\IsLocalMinOn\\ f\\ s\\ a \\land \\IsLocalMinOn\\ 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 \\IsLocalMinOn (x \\mapsto \\operatorname{op}(f(x))(g(x)))\\ s\\ a$$
Lean4
nonrec theorem bicomp_mono [Preorder δ] {op : β → γ → δ} (hop : ((· ≤ ·) ⇒ (· ≤ ·) ⇒ (· ≤ ·)) op op)
(hf : IsLocalMinOn f s a) {g : α → γ} (hg : IsLocalMinOn g s a) : IsLocalMinOn (fun x => op (f x) (g x)) s a :=
hf.bicomp_mono hop hg
