map_nhds_eq — Mathlib

English

If h: X ≃ₜ Y is a homeomorphism and x ∈ X, then the image of the neighborhood filter at x under h equals the neighborhood filter at h(x).

Русский

Если h: X ≃ₜ Y — гомеоморфизм и x ∈ X, то образ фильтра окрестностей x под действием h совпадает с окрестностями h(x).

LaTeX

$$$map\ h\ (\mathcal{N} x) = \mathcal{N}(h x).$$$

Lean4

@[simp]
theorem map_nhds_eq (h : X ≃ₜ Y) (x : X) : map h (𝓝 x) = 𝓝 (h x) :=
  h.isEmbedding.map_nhds_of_mem _ (by simp)

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