sigmaCompact

Mathlib.Topology.Compactness.SigmaCompact

URI: https://scilib.ai/kg/mathlib#CompactSpace.sigmaCompact

English

A compact space is σ-compact.

Русский

Компактное пространство σ-скомпактно.

LaTeX

$$$CompactSpace X \\rightarrow SigmaCompactSpace X$$$

Lean4

instance (priority := 200) sigmaCompact [CompactSpace X] : SigmaCompactSpace X :=
  ⟨⟨fun _ => univ, fun _ => isCompact_univ, iUnion_const _⟩⟩

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

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

Разделы

Аффилиация

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