instDiscreteTopologyULift

Mathlib.Topology.Constructions

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

English

If X is a discrete space, then ULift X is also discrete.

Русский

Если X имеет дискретную топологию, то ULift X также дискретно.

LaTeX

$$$\mathrm{DiscreteTopology}(\mathrm{ULift} X).$$$

Lean4

instance [TopologicalSpace X] [DiscreteTopology X] : DiscreteTopology (ULift X) :=
  IsEmbedding.uliftDown.discreteTopology

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

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

Разделы

Аффилиация

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