map_mk_nhdsSet

Mathlib.Topology.Inseparable

URI: https://scilib.ai/kg/mathlib#SeparationQuotient.map_mk_nhdsSet

English

The map of mk on nhdsSet s equals nhdsSet of mk s.

Русский

Образ mk на nhdsSet s равен nhdsSet mk''s.

LaTeX

$$$\\mathrm{map}(\\mathrm{mk}, \\mathcal{N}_{\\mathrm{set}}(s)) = \\mathcal{N}_{\\mathrm{set}}(\\mathrm{mk}''s)$$$

Lean4

theorem map_mk_nhdsSet : map mk (𝓝ˢ s) = 𝓝ˢ (mk '' s) := by
  rw [← comap_mk_nhdsSet_image, map_comap_of_surjective surjective_mk]

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

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

Разделы

Аффилиация

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