map_mk_nhds — Mathlib

English

The push-forward of the neighborhood under mk equals the neighborhood of the image.

Русский

Перемещение окрестности через mk дает окрестность образа.

LaTeX

$$$\\operatorname{map}(\\mathrm{mk}, \\mathcal{N}(x)) = \\mathcal{N}(\\mathrm{mk}(x))$$$

Lean4

/-- Push-forward of the neighborhood of a point along the projection to the separation quotient
is the neighborhood of its equivalence class. -/
theorem map_mk_nhds : map mk (𝓝 x) = 𝓝 (mk x) := by rw [← comap_mk_nhds_mk, map_comap_of_surjective surjective_mk]

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