English
If there exists a countable collection S of subsets whose union is X and each subset is compact, then X is σ-compact.
Русский
Если существует счётная коллекция подмножеств S, чьи объединения равняется X и каждое подмножество компактно, то X σ-скомпактно.
LaTeX
$$$S \\text{.Countable} \\rightarrow (\\forall s \\in S, IsCompact s) \\rightarrow (⋃₀ S = univ) \\rightarrow SigmaCompactSpace X$$$
Lean4
instance [SigmaCompactSpace Y] : SigmaCompactSpace (X ⊕ Y) :=
⟨⟨fun n => Sum.inl '' compactCovering X n ∪ Sum.inr '' compactCovering Y n, fun n =>
((isCompact_compactCovering X n).image continuous_inl).union
((isCompact_compactCovering Y n).image continuous_inr),
by
simp only [iUnion_union_distrib, ← image_iUnion, iUnion_compactCovering, image_univ, range_inl_union_range_inr]⟩⟩
