isCompact_compactCovering

Mathlib.Topology.Compactness.SigmaCompact

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

← MathLib Explorer

English

For each n, compactCovering X n is compact.

Русский

Для каждого n множество compactCovering X n компактно.

LaTeX

$$$\\forall n, IsCompact (compactCovering X n)$$$

Lean4

theorem isCompact_compactCovering (n : ℕ) : IsCompact (compactCovering X n) :=
  isCompact_accumulate (Classical.choose_spec SigmaCompactSpace.exists_compact_covering).1 n

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

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

Разделы

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

Аффилиация

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