map_nhds_of_mem

Mathlib.Topology.Maps.Basic

URI: https://scilib.ai/kg/mathlib#Topology.IsEmbedding.map_nhds_of_mem

English

If f is an embedding and range f ∈ 𝓝 (f x), then (𝓝 x).map f = 𝓝 (f x).

Русский

Если f — вложение и range f принадлежит 𝓝( f(x) ), тогда (𝓝 x).map f = 𝓝( f x ).

LaTeX

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

Lean4

theorem map_nhds_of_mem (hf : IsEmbedding f) (x : X) (h : range f ∈ 𝓝 (f x)) : (𝓝 x).map f = 𝓝 (f x) :=
  hf.1.map_nhds_of_mem x h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru