English
Let f be locally minimal on s at a, and suppose there exist lower-neighborhood points of f(a) arbitrarily close from below and above. Then the neighborhood of f(a) is not contained in the image under f of any neighborhood of a restricted to s.
Русский
Пусть f имеет локальный минимум на s в точке a, и существуют точки произвольной близости к f(a) слева и справа. Тогда множество 𝓝(f(a)) не содержится в образе подмножества 𝓝[s] a под действием f.
LaTeX
$$$\mathrm{IsLocalMinOn}(f,s,a) \land \big(\mathcal{N}_{[<]}(f(a))\big).\mathrm{NeBot} \land \big(\mathcal{N}_{[>]}(f(a))\big).\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 : IsLocalMinOn f s a) [NeBot (𝓝[<] f a)] : ¬𝓝 (f a) ≤ map f (𝓝[s] a) :=
fun hle =>
have : ∀ᶠ y in 𝓝[<] f a, f a ≤ y := (eventually_map.2 hf).filter_mono (inf_le_left.trans hle)
let ⟨_y, hy⟩ := (this.and self_mem_nhdsWithin).exists
hy.1.not_gt hy.2
