English
If range f is in the neighborhood filter of f(a), then map f (nhds a) = nhds (f a).
Русский
Если range f содержится в окрестностном фильтре f(a), то map f (nhds a) = nhds (f a).
LaTeX
$$$\\text{If } range\\ f \\in 𝓝 (f a),\\; \\operatorname{map} f (\\mathcal{N}_{\\mathrm{induced}\\ f}(a)) = \\mathcal{N}(f a).$$$
Lean4
theorem map_nhds_induced_of_mem {a : α} (h : range f ∈ 𝓝 (f a)) : map f (@nhds α (induced f t) a) = 𝓝 (f a) := by
rw [nhds_induced, Filter.map_comap_of_mem h]