map_nhds_induced_of_surjective — Mathlib

English

If f: β → α is surjective, then for any a ∈ β, map f (nhds a) = nhds (f a) when using the induced topology on β.

Русский

Если отображение f: β → α сюръективно, то для любого a ∈ β отображение map f (nhds a) равно nhds (f a) в индуцированной топологии на β.

LaTeX

$$$\\text{Surjective } f \\Rightarrow \\forall a,\\; \\operatorname{map} f (\\mathcal{N}_{\\text{induced } f T}(a)) = \\mathcal{N}(f a).$$$

Lean4

theorem map_nhds_induced_of_surjective [T : TopologicalSpace α] {f : β → α} (hf : Surjective f) (a : β) :
    map f (@nhds β (TopologicalSpace.induced f T) a) = 𝓝 (f a) := by rw [nhds_induced, map_comap_of_surjective hf]

Похожие утверждения