instT4Space

Mathlib.Topology.Separation.Regular

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

English

If X is a T5 space, then ULift X is a T5 space.

Русский

Если X — T5-пространство, то ULift(X) — T5-пространство.

LaTeX

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

Lean4

instance instT4Space [T4Space X] : T4Space (ULift X) :=
  IsClosedEmbedding.uliftDown.t4Space

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

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

Разделы

Аффилиация

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