iUnion_compactCovering

Mathlib.Topology.Compactness.SigmaCompact

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

← MathLib Explorer

English

The union over n of compactCovering X n equals univ.

Русский

Объединение по n от compactCovering X n равно универсууму.

LaTeX

$$$\\bigcup_{n} compactCovering X n = univ$$$

Lean4

theorem iUnion_compactCovering : ⋃ n, compactCovering X n = univ :=
  by
  rw [compactCovering, iUnion_accumulate]
  exact (Classical.choose_spec SigmaCompactSpace.exists_compact_covering).2

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

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

Разделы

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

Аффилиация

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