compactSpace

Mathlib.Topology.Homeomorph.Lemmas

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

English

If X is a compact space and h: X ≃ Y is a homeomorphism, then Y is also compact.

Русский

Если X — компактное пространство, и h: X ≃ Y — гомеоморфизм, тогда и Y компактно.

LaTeX

$$$LocallyCompactSpace X \\Rightarrow LocallyCompactSpace Y$$$

Lean4

protected theorem compactSpace [CompactSpace X] (h : X ≃ₜ Y) : CompactSpace Y where
  isCompact_univ := h.symm.isCompact_preimage.2 isCompact_univ

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

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

Разделы

Аффилиация

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