English
Countable unions of σ-compact sets indexed by a finite set are σ-compact.
Русский
Ловимая сумма конечного множества σ-компактных множеств образует σ-компактное множество.
LaTeX
$$$s : Set ι\, S : ι → Set X\, (hc : Set.Countable s) (hcomp : \forall i ∈ s, IsSigmaCompact (S i)) : IsSigmaCompact(\bigcup (i : ι) (h : i ∈ s), S i)$$$
Lean4
/-- Countable unions of σ-compact sets are σ-compact. -/
theorem isSigmaCompact_iUnion [Countable ι] (s : ι → Set X) (hcomp : ∀ i, IsSigmaCompact (s i)) :
IsSigmaCompact (⋃ i, s i) := by
-- Choose a decomposition s_i = ⋃ K_i,j for each i.
choose K hcomp hcov using fun i ↦ hcomp i
have :=
calc
⋃ i, s i
_ = ⋃ i, ⋃ n, (K i n) := by simp_rw [hcov]
_ = ⋃ (i) (n : ℕ), (K.uncurry ⟨i, n⟩) := by rw [Function.uncurry_def]
_ = ⋃ x, K.uncurry x := by rw [← iUnion_prod']
rw [this]
exact isSigmaCompact_iUnion_of_isCompact K.uncurry fun x ↦ (hcomp x.1 x.2)
