nhds_mk

Mathlib.Topology.Inseparable

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

English

The neighborhood filter of mk x equals map mk of nhds x.

Русский

Окрестностная фильтра mk x равна образу mk окрестностей x.

LaTeX

$$$\\mathrm{nhds}(\\mathrm{mk}(x)) = \\operatorname{map}(\\mathrm{mk}, \\mathrm{nhds}(x))$$$

Lean4

@[deprecated map_mk_nhds (since := "2025-03-21")]
theorem nhds_mk (x : X) : 𝓝 (mk x) = .map mk (𝓝 x) :=
  .symm <| map_mk_nhds ..

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

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

Разделы

Аффилиация

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