English
Let f and g be functions from a topological space to a preordered set. If f has a local maximum at a point a and f and g agree in a neighborhood of a (i.e., f and g are eventually equal near a), then g also has a local maximum at a.
Русский
Пусть f и g — функции из топологического пространства в упорядоченное множество. Если f имеет локальный максимум в точке a, и если f и g совпадают в окрестности a (то есть они эквивалентны по nhds a на этапе), то и у g в той же точке a есть локальный максимум.
LaTeX
$$$\\forall {\\alpha, \\beta}, \\;$ пусть f,g : $\\alpha \\to \\beta$ и $a \\in \\alpha$. Если $IsLocalMax(f,a)$ и $f =_{\\mathcal{N}a}^{\\mathrm{!-ev}} g$, тогда $IsLocalMax(g,a)$, где $f =^{\\mathcal{N}a}_{\\mathrm{ev}} g$ означает локальное совпадение около $a$.$$
Lean4
nonrec theorem congr {f g : α → β} {a : α} (h : IsLocalMax f a) (heq : f =ᶠ[𝓝 a] g) : IsLocalMax g a :=
h.congr heq heq.eq_of_nhds
