instT1SpaceOfT0SpaceOfR0Space

Mathlib.Topology.Separation.Basic

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

English

If X is T0 and R0, then X is T1.

Русский

Если X является T0 и R0 пространством, то X является T1.

LaTeX

$$$T0Space X ∧ R0Space X ⇒ T1Space X$.$$

Lean4

instance (priority := 80) [T0Space X] [R0Space X] : T1Space X :=
  t1Space_iff_t0Space_and_r0Space.mpr ⟨‹T0Space X›, ‹R0Space X›⟩

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

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

Разделы

Аффилиация

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