English
Let op: a binary operation op with monotone in each argument. If f and g have local minima at a, then x ↦ op(f(x), g(x)) has a local minimum at a.
Русский
Пусть бинарная операция op монотонна по каждому аргументу. Если f и g имеют локальные минимумы в a, то x ↦ op(f(x), g(x)) имеет локальный минимум в a.
LaTeX
$$$Hop:\; (\le) \Rightarrow (\le) \Rightarrow (\le) op op) \land \mathrm{IsLocalMin}(f,a) \land \mathrm{IsLocalMin}(g,a) \Rightarrow \mathrm{IsLocalMin}(\lambda x. op(f(x), g(x)), a)$$$
Lean4
nonrec theorem bicomp_mono [Preorder δ] {op : β → γ → δ} (hop : ((· ≤ ·) ⇒ (· ≤ ·) ⇒ (· ≤ ·)) op op)
(hf : IsLocalMin f a) {g : α → γ} (hg : IsLocalMin g a) : IsLocalMin (fun x => op (f x) (g x)) a :=
hf.bicomp_mono hop hg
