t2Space_iff_t0Space

Mathlib.Topology.Separation.Hausdorff

URI: https://scilib.ai/kg/mathlib#R1Space.t2Space_iff_t0Space

English

In an R1 space, T2 is equivalent to T0.

Русский

В пространстве с R1 свойство T2 эквивалентно T0.

LaTeX

$$$ [R1Space X] \Rightarrow (\operatorname{T2Space}(X) \iff \operatorname{T0Space}(X)) $$$

Lean4

theorem t2Space_iff_t0Space [R1Space X] : T2Space X ↔ T0Space X := by constructor <;> intro <;> infer_instance

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

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

Разделы

Аффилиация

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