min — Mathlib

English

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

Русский

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

Lean4

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

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