biUnion — Mathlib

English

The union of finitely many Gδ sets is a Gδ set, bounded indexed union version.

Русский

Объединение конечного числа Gδ множеств является Gδ, в зависимости от ограниченного индекса.

LaTeX

$$$S.Finite \\Rightarrow (\\forall i\\in S, IsGδ(f(i))) \\Rightarrow IsGδ(\\bigcup_{i\\in S} f(i))$$$

Lean4

/-- The union of finitely many Gδ sets is a Gδ set, bounded indexed union version. -/
theorem biUnion {s : Set ι} (hs : s.Finite) {f : ι → Set X} (h : ∀ i ∈ s, IsGδ (f i)) : IsGδ (⋃ i ∈ s, f i) :=
  by
  rw [← sUnion_image]
  exact .sUnion (hs.image _) (forall_mem_image.2 h)

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