t0Space

Mathlib.Topology.Separation.Basic

URI: https://scilib.ai/kg/mathlib#T1Space.t0Space

English

If X is a T1-space, then X is a T0-space.

Русский

Если X — T1-пространство, то оно также является T0-пространством.

LaTeX

$$$ [T1Space X] \Rightarrow T0Space X$.$$

Lean4

instance (priority := 100) t0Space [T1Space X] : T0Space X :=
  (t1Space_iff_t0Space_and_r0Space.mp ‹T1Space X›).left

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

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

Разделы

Аффилиация

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