isLocalExtr_iff — Mathlib

English

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

Русский

Если f и g равны в окрестности a, то IsLocalExtr f a эквивалентно IsLocalExtr g a.

LaTeX

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

Lean4

theorem isLocalExtr_iff {f g : α → β} {a : α} (heq : f =ᶠ[𝓝 a] g) : IsLocalExtr f a ↔ IsLocalExtr g a :=
  heq.isExtrFilter_iff heq.eq_of_nhds

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