iUnion — Mathlib

English

The union of finitely many Gδ sets (bounded index) is a Gδ set.

Русский

Объединение конечного набора Gδ множеств — это Gδ.

LaTeX

$$$[Finite\\ ι']\\ {f: ι'→Set X}\\ (\\forall i, IsGδ(f(i)))\\Rightarrow IsGδ(\\bigcup_{i} f(i))$$$

Lean4

/-- The union of finitely many Gδ sets is a Gδ set, bounded indexed union version. -/
theorem iUnion [Finite ι'] {f : ι' → Set X} (h : ∀ i, IsGδ (f i)) : IsGδ (⋃ i, f i) :=
  .sUnion (finite_range _) <| forall_mem_range.2 h

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