isLocalMax — Mathlib

English

If nhds a within s eventually leads to g ≤ f and f(a) = g(a), and f has a local maximum on s at a, then g also has a local maximum on s at a.

Русский

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

LaTeX

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

Lean4

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

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