max — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

nonrec theorem max (hf : IsLocalMax f a) (hg : IsLocalMax g a) : IsLocalMax (fun x => max (f x) (g x)) a :=
  hf.max hg

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