instR0SpaceOfT1Space

Mathlib.Topology.Separation.Basic

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

English

From a T1 structure, one obtains an R0 space structure; hence T0 and R0 hold together to give T1.

Русский

Из T1-пространства следует R0-пространство; вместе с T0 обеспечивает T1.

LaTeX

$$R0Space X follows from T1Space X; thus T0Space X ∧ R0Space X.$$

Lean4

instance (priority := 100) [T1Space X] : R0Space X :=
  (t1Space_iff_t0Space_and_r0Space.mp ‹T1Space X›).right

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

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

Разделы

Аффилиация

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