max — Mathlib

English

If f and g have local minima on s at a, then the function x ↦ max(f(x), g(x)) 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 max (hf : IsLocalMin f a) (hg : IsLocalMin g a) : IsLocalMin (fun x => max (f x) (g x)) a :=
  hf.max hg

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