map_nhds_eq — Mathlib

English

For an embedding f, the image of the neighborhood filter at x equals the neighborhood filter at f(x) restricted to range f: (𝓝 x).map f = 𝓝[range f] (f x).

Русский

Для вложения f изображение фильтра окрестностей в точке x равно окрестностям в f(x) ограниченным до диапазона f: (𝓝 x).map f = 𝓝[range f](f(x)).

LaTeX

$$$(\mathcal{N} x).map f = \mathcal{N}_{\mathrm{range}(f)}(f x)$$$

Lean4

theorem map_nhds_eq (hf : IsEmbedding f) (x : X) : (𝓝 x).map f = 𝓝[range f] f x :=
  hf.1.map_nhds_eq x

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