map_nhds_eq — Mathlib

English

For an open quotient map f, map f sends nhds to nhds: map f (𝓝 x) = 𝓝 (f x).

Русский

При открытом факторном отображении f отображение окрестности сохраняется: map f (𝓝 x) = 𝓝 (f x).

LaTeX

$$$\mathrm{map}(f, \mathcal{N}(x)) = \mathcal{N}(f(x))$ under IsOpenQuotientMap f$$

Lean4

theorem map_nhds_eq (h : IsOpenQuotientMap f) (x : X) : map f (𝓝 x) = 𝓝 (f x) :=
  le_antisymm h.continuous.continuousAt <| h.isOpenMap.nhds_le _

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