isLocalMaxOn — Mathlib

English

If nhdsWithin a set s at a sees f and g eventually equal and f has a local minimum on s at a, then g also has a local minimum on s at a.

Русский

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

LaTeX

$$$\forall {f,g: \alpha \to \beta} {a: \alpha} {s: Set\alpha},\; (nhdsWithin a s).EventuallyLE f g \to Eq (f a) (g a) \to IsLocalMinOn f s a \to IsLocalMinOn g s a$$$

Lean4

theorem isLocalMaxOn {f g : α → β} {a : α} (hle : g ≤ᶠ[𝓝[s] a] f) (hfga : f a = g a) (h : IsLocalMaxOn f s a) :
    IsLocalMaxOn g s a :=
  hle.isMaxFilter hfga h

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