nhds_eq_comap — Mathlib

English

For a homeomorphism h: X ≃ₜ Y and x ∈ X, the neighborhood filter at x equals the comap of the neighborhood filter at h(x) along h.

Русский

Для гомеоморфизма h: X ≃ₜ Y и точки x ∈ X окрестности x равны обратному образу окрестностей h(x) по h.

LaTeX

$$$\mathcal{N}(x) = \mathrm{comap}\; h\ (\mathcal{N}(h x)).$$$

Lean4

theorem nhds_eq_comap (h : X ≃ₜ Y) (x : X) : 𝓝 x = comap h (𝓝 (h x)) :=
  h.isInducing.nhds_eq_comap x

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