isLocalMin_iff — Mathlib

English

If f and g are Eventually Equal near a, then IsLocalMin f a iff IsLocalMin g a.

Русский

Если f и g равны позднее по nhds a, то локальный минимум f в a эквивалентен локальному минимуму g в a.

LaTeX

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

Lean4

theorem isLocalMin_iff {f g : α → β} {a : α} (heq : f =ᶠ[𝓝 a] g) : IsLocalMin f a ↔ IsLocalMin g a :=
  heq.isMinFilter_iff heq.eq_of_nhds

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