map_nhds_eq — Mathlib

English

If f is a local homeomorph on s, then the nhds map respects f: the map of neighborhoods at x equals the neighborhood of f(x).

Русский

Для локального гомеоморфизма f верно отображение окрестностей: nhds x под действием f совпадает с nhds (f x).

LaTeX

$$$\\forall x \\in s, (\\mathcal{N}_x) \\;\\text{ maps to } \\mathcal{N}_{f(x)}$ under $f$.$$

Lean4

theorem map_nhds_eq (hf : IsLocalHomeomorphOn f s) {x : X} (hx : x ∈ s) : (𝓝 x).map f = 𝓝 (f x) :=
  let ⟨e, hx, he⟩ := hf x hx
  he.symm ▸ e.map_nhds_eq hx

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