exists_compact_covering — Mathlib

English

Existence of a countable compact covering for a σ-compact space.

Русский

Существование счётного покрытия компактами для σ-компактного пространства.

LaTeX

$$$\\exists K : \\mathbb{N} \\to Set X, (\\forall n, IsCompact (K n)) \\land ⋃ n, K n = univ$$$

Lean4

theorem exists_compact_covering [h : SigmaCompactSpace X] : ∃ K : ℕ → Set X, (∀ n, IsCompact (K n)) ∧ ⋃ n, K n = univ :=
  SigmaCompactSpace_iff_exists_compact_covering.mp h

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