English
Two functions that are eventually equal near a within s share the same local extremality on s at a.
Русский
Две функции, которые равны почти в окрестности a внутри s, имеют одно и то же локальное экстремальное поведение на s в a.
LaTeX
$$$\forall {f g: \alpha \to \beta} {a: \alpha} {s: Set\alpha},\; (nhdsWithin a s).EventuallyEq f g \to Set.instMembership.mem s a \to IsLocalExtrOn f s a \leftrightarrow IsLocalExtrOn g s a$$$
Lean4
theorem isLocalExtrOn_iff {f g : α → β} {a : α} (heq : f =ᶠ[𝓝[s] a] g) (hmem : a ∈ s) :
IsLocalExtrOn f s a ↔ IsLocalExtrOn g s a :=
heq.isExtrFilter_iff <| heq.eq_of_nhdsWithin hmem