compactSpace

Mathlib.Topology.Compactness.Compact

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

English

If X is a compact space, then the lifted space ULift X is also compact.

Русский

Если X компактно, то ULift X также компактно.

LaTeX

$$$\text{CompactSpace}(X) \Rightarrow \text{CompactSpace}(\mathrm{ULift}(X))$$$

Lean4

instance compactSpace [CompactSpace X] : CompactSpace (ULift.{v} X) :=
  IsClosedEmbedding.uliftDown.compactSpace

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

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

Разделы

Аффилиация

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