instT1Space

Mathlib.Topology.Separation.Basic

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

English

If X is a T1-space, then ULift X is a T1-space.

Русский

Если X — T1-пространство, то ULift X — тоже T1-пространство.

LaTeX

$$$ \text{T1Space X} \Rightarrow \text{T1Space (ULift X)}$.$$

Lean4

instance instT1Space [T1Space X] : T1Space (ULift X) :=
  IsEmbedding.uliftDown.t1Space

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

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

Разделы

Аффилиация

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