English
For a ∈ α, map f (nhds a) equals nhdsWithin (range f) (f a) when using induced topology by f.
Русский
Для фиксированного a: α отображение map f от nhds a равно nhdsWithin (range f) (f a) в индуцированной топологии через f.
LaTeX
$$$\\text{map } f (\\mathcal{N}_{\\mathrm{induced}\\ f\\ t}(a)) = \\mathcal{N}_{\\mathrm{within}} (\\mathrm{range}(f)) (f(a)).$$$
Lean4
theorem map_nhds_induced_eq (a : α) : map f (@nhds α (induced f t) a) = 𝓝[range f] f a := by
rw [nhds_induced, Filter.map_comap, nhdsWithin]