English
Let f have a local extremum on s at a, and suppose there exist both left and right neighborhoods of f(a). Then 𝓝(f(a)) is not contained in the image of any nhdsWithin(a,s) under f.
Русский
Пусть f имеет локальный экстремум на s в точке a, и существуют окрестности слева и справа от f(a). Тогда 𝓝(f(a)) не содержится в образе 𝓝[s](a) под f.
LaTeX
$$$\mathrm{IsLocalExtrOn}(f,s,a) \land ((\mathcal{N}_{[<]}(f(a))).\mathrm{NeBot}) \land ((\mathcal{N}_{[>]}(f(a))).\mathrm{NeBot}) \Rightarrow \neg\big(\mathcal{N}(f(a)) \le map\ f\ (\mathcal{N}[s](a))\big)$$$
Lean4
theorem not_nhds_le_map [TopologicalSpace β] (hf : IsLocalExtrOn f s a) [NeBot (𝓝[<] f a)] [NeBot (𝓝[>] f a)] :
¬𝓝 (f a) ≤ map f (𝓝[s] a) :=
hf.elim (fun h => h.not_nhds_le_map) fun h => h.not_nhds_le_map
