instT2Space

Mathlib.Topology.Separation.Hausdorff

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

English

If X is Hausdorff, then ULift X is also Hausdorff.

Русский

Если X — Хаусдорфово пространство, то ULift X также Хаусдорфово.

LaTeX

$$$ \\forall X\\,[TopologicalSpace\\ X] \\ [T2Space\\ X] \\Rightarrow T2Space(ULift\\ X)$$$

Lean4

instance instT2Space [T2Space X] : T2Space (ULift X) :=
  IsEmbedding.uliftDown.t2Space

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

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

Разделы

Аффилиация

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