ker_nhds

Mathlib.Topology.Separation.Basic

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

English

In a T1 space, the kernel of the neighborhood filter at a point x is the singleton {x}.

Русский

В T1-пространстве ядро фильтра окрестностей в точке x равно {x}.

LaTeX

$$$(\nhds x).\ker = \{ x \}$$$

Lean4

@[simp]
theorem ker_nhds [T1Space X] (x : X) : (𝓝 x).ker = { x } := by simp [ker_nhds_eq_specializes]

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

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

Разделы

Аффилиация

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