instT4SpaceOfT1SpaceOfNormalSpace

Mathlib.Topology.Separation.Regular

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

English

If X is T1 and normal, then X is T4.

Русский

Если X — T1-пространство и нормальное, то X — T4.

LaTeX

$$$ [T1Space X] \\land [NormalSpace X] \\Rightarrow [T4Space X]$$$

Lean4

instance (priority := 100) [T1Space X] [NormalSpace X] : T4Space X :=
  ⟨⟩
    -- see Note [lower instance priority]

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

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

Разделы

Аффилиация

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