t1Space_iff_disjoint_nhds_pure

Mathlib.Topology.Separation.Basic

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

English

In a T1 space, specialization relation between x and y is equivalent to x = y.

Русский

В T1-пространстве отношение специализации между точками x и y эквивалентно x = y.

LaTeX

$$$Specializes(x,y) \\iff x = y$ in a T1Space.$$

Lean4

theorem t1Space_iff_disjoint_nhds_pure : T1Space X ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y) :=
  (t1Space_TFAE X).out 0 7

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

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

Разделы

Аффилиация

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