compactSpace

Mathlib.Topology.NoetherianSpace

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.NoetherianSpace.compactSpace

English

Every Noetherian space is compact.

Русский

Любое пространство Ноetherian компактно.

LaTeX

$$$\\text{CompactSpace}(\\alpha)\\quad\\text{when }\\text{NoetherianSpace}(\\alpha).$$$

Lean4

instance (priority := 100) compactSpace [h : NoetherianSpace α] : CompactSpace α :=
  ⟨(noetherianSpace_iff_opens α).mp h ⊤⟩

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

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

Разделы

Аффилиация

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