min — Mathlib

English

If f has a local minimum on s at a and f and g are eventually equal near a within s, then g also has a local minimum on s at a.

Русский

Если f имеет локальный минимум на s в a и f и g совпадают ближе к a внутри s, то и g имеет локальный минимум на s в a.

LaTeX

$$$\forall {f,g: \alpha \to \beta} {a: \alpha} {s: Set\alpha},\; IsLocalMinOn f s a \to (f =^\!/_{\mathcal{N}[s] a} g) \to a \in s \to IsLocalMinOn g s a$$$

Lean4

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

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