comap_sigmaMk_nhds

Mathlib.Topology.Constructions

URI: https://scilib.ai/kg/mathlib#comap_sigmaMk_nhds

English

The comap of nhds ⟨i,x⟩ along Sigma.mk i equals nhds x.

Русский

Обратное образование nhds ⟨i,x⟩ по Sigma.mk i равно nhds x.

LaTeX

$$$\\operatorname{comap}(\\Sigma.mk\\ i)(\\mathcal{N}(\\langle i,x\\rangle)) = \\mathcal{N}(x)$$$

Lean4

theorem comap_sigmaMk_nhds (i : ι) (x : σ i) : comap (Sigma.mk i) (𝓝 ⟨i, x⟩) = 𝓝 x :=
  (IsEmbedding.sigmaMk.nhds_eq_comap _).symm

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

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

Разделы

Аффилиация

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