map_nhds_eq — Mathlib

English

If f is a local homeomorphism, then for any x ∈ X, the image of the neighborhood filter of x under f is the neighborhood filter of f(x).

Русский

Если f — локальная гомеоморфия, то для любого x ∈ X образ фильтра окрестностей x под f равен фильтру окрестностей f(x).

LaTeX

$$$\operatorname{IsLocalHomeomorph}(f) \Rightarrow \forall x, \mathcal{N}_{x} \mapsto f = \mathcal{N}_{f(x)}$$$

Lean4

theorem map_nhds_eq (hf : IsLocalHomeomorph f) (x : X) : (𝓝 x).map f = 𝓝 (f x) :=
  hf.isLocalHomeomorphOn.map_nhds_eq (Set.mem_univ x)

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