symm_map_nhds_eq — Mathlib

English

If h: X ≃ₜ Y is a homeomorphism and x ∈ X, then map h.symm applied to 𝓝(h(x)) yields 𝓝(x).

Русский

Если h: X ≃ₜ Y — гомеоморфизм и x ∈ X, то отображение через h.symm переводит 𝓝(h(x)) в 𝓝(x).

LaTeX

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

Lean4

theorem symm_map_nhds_eq (h : X ≃ₜ Y) (x : X) : map h.symm (𝓝 (h x)) = 𝓝 x := by
  rw [h.symm.map_nhds_eq, h.symm_apply_apply]

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