of_countable — Mathlib

English

If there exists a countable collection S of subsets of X such that each member is compact and their union is all of X, then X is σ-compact.

Русский

Если существует счётная совокупность подмножеств S ⊆ P(X), каждое из которых компактно, и их объединение равно X, то X σ-скомпактно.

LaTeX

$$$S \\text{ countable} \\rightarrow (\\forall s \\in S, IsCompact s) \\rightarrow (⋃₀ S = univ) \\rightarrow SigmaCompactSpace X$$$

Lean4

theorem of_countable (S : Set (Set X)) (Hc : S.Countable) (Hcomp : ∀ s ∈ S, IsCompact s) (HU : ⋃₀ S = univ) :
    SigmaCompactSpace X :=
  ⟨(exists_seq_cover_iff_countable ⟨_, isCompact_empty⟩).2 ⟨S, Hc, Hcomp, HU⟩⟩
    -- see Note [lower instance priority]

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