English
If two functions f and g are Eventually Equal near a, then f has a local maximum at a if and only if g has a local maximum at a.
Русский
Если две функции f и g равны на окрестности точки a до какого-либо момента (EventuallyEq near a), то f имеет локальный максимум в a тогда и только тогда, когда g имеет локальный максимум в a.
LaTeX
$$$\\forall {f,g:\\alpha\\to\\beta}, \\forall a:\\alpha,\\ (f =^{\\ NHds a}_{\\mathrm{ev}} g) \\Rightarrow (IsLocalMax f a \\iff IsLocalMax g a)$$$
Lean4
theorem isLocalMax_iff {f g : α → β} {a : α} (heq : f =ᶠ[𝓝 a] g) : IsLocalMax f a ↔ IsLocalMax g a :=
heq.isMaxFilter_iff heq.eq_of_nhds