noncompact_univ

Mathlib.Topology.Compactness.Compact

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

English

If X is noncompact, then the whole space X is not compact.

Русский

Если X не компактно, то всё пространство X не является компактным.

LaTeX

$$$\neg IsCompact(\mathrm{univ})$$$

Lean4

theorem noncompact_univ (X : Type*) [TopologicalSpace X] [NoncompactSpace X] : ¬IsCompact (univ : Set X) :=
  NoncompactSpace.noncompact_univ

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

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

Разделы

Аффилиация

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