isSigmaCompact_sUnion — Mathlib

English

Countable unions of σ-compact sets are σ-compact.

Русский

Счётное объединение σ-компактных множеств σ-компактно.

LaTeX

$$$\\text{IsSigmaCompact}(\\bigcup_{s\\in S} s) \\text{ if } S \\text{ countable and each } s \\in S \\text{ is σ-compact}$$$

Lean4

/-- Countable unions of σ-compact sets are σ-compact. -/
theorem isSigmaCompact_sUnion (S : Set (Set X)) (hc : Set.Countable S) (hcomp : ∀ s : S, IsSigmaCompact s (X := X)) :
    IsSigmaCompact (⋃₀ S) := by
  have : Countable S := countable_coe_iff.mpr hc
  apply sUnion_eq_iUnion.symm ▸ isSigmaCompact_iUnion _ hcomp

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