isSigmaCompact_sUnion_of_isCompact

English

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

Русский

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

LaTeX

$$$S : Set (Set X)\, (hc : Set.Countable S) (hcomp : \forall s ∈ S, IsSigmaCompact s) : IsSigmaCompact(\bigcup S)$$$

Lean4

/-- Countable unions of compact sets are σ-compact. -/
theorem isSigmaCompact_sUnion_of_isCompact {S : Set (Set X)} (hc : Set.Countable S)
    (hcomp : ∀ (s : Set X), s ∈ S → IsCompact s) : IsSigmaCompact (⋃₀ S) :=
  by
  have : Countable S := countable_coe_iff.mpr hc
  rw [sUnion_eq_iUnion]
  apply isSigmaCompact_iUnion_of_isCompact _ (fun ⟨s, hs⟩ ↦ hcomp s hs)

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