min — Mathlib

English

If f and g have local minima on s at a, then the function x ↦ max(f(x), g(x)) also has a local minimum at a.

Русский

Если f и g имеют локальные минимумы на s в a, то максимум по значениям max(f(x), g(x)) имеет локальный минимум в a.

LaTeX

$$$\forall {f,g: \alpha \to \beta} {a: \alpha} {s: Set\alpha},\; IsLocalMinOn f s a \to IsLocalMinOn g s a \to IsLocalMinOn (\\lambda x. max (f(x)) (g(x))) s a$$$

Lean4

nonrec theorem min (hf : IsLocalMaxOn f s a) (hg : IsLocalMaxOn g s a) : IsLocalMaxOn (fun x => min (f x) (g x)) s a :=
  hf.min hg

Похожие утверждения