isLocalMinOn — Mathlib

English

If f ≤ᶠ near a within s of g and f(a) = g(a) and f has a local minimum on s at a, then g has a local minimum on s at a.

Русский

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

LaTeX

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

Lean4

theorem isLocalMinOn {f g : α → β} {a : α} (hle : f ≤ᶠ[𝓝[s] a] g) (hfga : f a = g a) (h : IsLocalMinOn f s a) :
    IsLocalMinOn g s a :=
  hle.isMinFilter hfga h

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