isSigmaCompact

Mathlib.Topology.Compactness.SigmaCompact

URI: https://scilib.ai/kg/mathlib#IsCompact.isSigmaCompact

← MathLib Explorer

English

Every compact set is σ-compact.

Русский

Каждое компактное множество является σ-компактным.

LaTeX

$$$\text{IsCompact}(s) \Rightarrow \text{IsSigmaCompact}(s)$$$

Lean4

/-- Compact sets are σ-compact. -/
theorem isSigmaCompact {s : Set X} (hs : IsCompact s) : IsSigmaCompact s :=
  ⟨fun _ => s, fun _ => hs, iUnion_const _⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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