SigmaCompactSpace_iff_exists_compact_covering

English

A space is σ-compact iff there exists a countable family of compact subspaces covering the entire space.

Русский

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

LaTeX

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

Lean4

/-- A topological space is σ-compact iff there exists a countable collection of compact
subspaces that cover the entire space. -/
theorem SigmaCompactSpace_iff_exists_compact_covering :
    SigmaCompactSpace X ↔ ∃ K : ℕ → Set X, (∀ n, IsCompact (K n)) ∧ ⋃ n, K n = univ := by
  rw [← isSigmaCompact_univ_iff, IsSigmaCompact]

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