Theorems · Theorem · general topology

isSigmaCompact_iUnion_of_isCompact

∀ {X : Type u_1} {ι : Type u_3} [inst : TopologicalSpace X] [hι : Countable ι] (s : ι → Set X),
  (∀ (i : ι), IsCompact (s i)) → IsSigmaCompact (⋃ i, s i)

Countable unions of compact sets are σ-compact.

Defined in

Mathlib.Topology.Compactness.SigmaCompact

Cited by

2 results in Mathlib

Foundations

Depth 64 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceCountable