isLocalMin — Mathlib

English

If f is EventuallyLessOrEqual to g near a, and f(a) = g(a), and f has a local minimum at a, then g also has a local minimum at a.

Русский

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

LaTeX

$$$\\forall f,g: \\alpha \\to \\beta, \\forall a:\\alpha, (f \\leq^{\\ NHds a}_{\\mathrm{ev}} g) \\land (f(a)=g(a)) \\land IsLocalMin f a \\Rightarrow IsLocalMin g a$$$

Lean4

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

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