instT2SpaceOfR1SpaceOfT0Space

Mathlib.Topology.Separation.Hausdorff

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

← MathLib Explorer

English

A space with both R1 and T0 properties is Hausdorff.

Русский

Пространство с свойствами R1 и T0 является хаусдорфовым.

LaTeX

$$$ [\text{R1Space } X] \land [\text{T0Space } X] \Rightarrow \text{T2Space } X $$$

Lean4

instance (priority := 80) [R1Space X] [T0Space X] : T2Space X :=
  t2Space_iff_disjoint_nhds.2 fun _x _y hne ↦ disjoint_nhds_nhds_iff_not_inseparable.2 fun hxy ↦ hne hxy.eq

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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