instCompletelyNormalSpace

Mathlib.Topology.Separation.Regular

URI: https://scilib.ai/kg/mathlib#ULift.instCompletelyNormalSpace

English

If X is completely normal, then ULift X is completely normal.

Русский

Если X полностью нормальное, то ULift(X) полностью нормальное.

LaTeX

$$$ [CompletelyNormalSpace X] \\Rightarrow [CompletelyNormalSpace(ULift X)]$$$

Lean4

instance instCompletelyNormalSpace [CompletelyNormalSpace X] : CompletelyNormalSpace (ULift X) :=
  IsEmbedding.uliftDown.completelyNormalSpace

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

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

Разделы

Аффилиация

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