min — Mathlib

English

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

Русский

Если f и g имеют локальные максимумы на s в a, то минимальное по значению min(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. \min (f(x)) (g(x))) s a$$$

Lean4

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

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