isSigmaCompact_biUnion — Mathlib

English

A finite union of σ-compact sets is σ-compact.

Русский

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

LaTeX

$$$s : Set ι\, S : ι → Set X\, t : Set ι\, (t.Finite) (hcomp : \forall i ∈ t, IsSigmaCompact (S i)) : IsSigmaCompact (⋃ i ∈ t, S i)$$$

Lean4

/-- Countable unions of σ-compact sets are σ-compact. -/
theorem isSigmaCompact_biUnion {s : Set ι} {S : ι → Set X} (hc : Set.Countable s)
    (hcomp : ∀ (i : ι), i ∈ s → IsSigmaCompact (S i)) : IsSigmaCompact (⋃ (i : ι) (_ : i ∈ s), S i) :=
  by
  have : Countable ↑s := countable_coe_iff.mpr hc
  rw [biUnion_eq_iUnion]
  exact isSigmaCompact_iUnion _ (fun ⟨i', hi'⟩ ↦ hcomp i' hi')

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