map_nhds_eq — Mathlib

English

The image of a neighborhood under e equals the neighborhood of the image.

Русский

Образ окрестности под e равен окрестности образа.

LaTeX

$$$\\mathrm{map}\\,e\\; (\\mathcal{N}\\!\\!\\!\\! (x)) = \\mathcal{N}\\!\\!\\!\\! (e(x))$$$

Lean4

theorem map_nhds_eq {x} (hx : x ∈ e.source) : map e (𝓝 x) = 𝓝 (e x) :=
  le_antisymm (e.continuousAt hx) <| le_map_of_right_inverse (e.eventually_right_inverse' hx) (e.tendsto_symm hx)

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