sUnion — Mathlib

English

The union of finitely many Gδ sets is a Gδ set.

Русский

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

LaTeX

$$$S.Finite \\Rightarrow (\\forall s\\in S, IsGδ(s)) \\Rightarrow IsGδ(\\bigcup_0 S)$$$

Lean4

/-- The union of finitely many Gδ sets is a Gδ set, `Set.sUnion` version. -/
theorem sUnion {S : Set (Set X)} (hS : S.Finite) (h : ∀ s ∈ S, IsGδ s) : IsGδ (⋃₀ S) := by
  induction S, hS using Set.Finite.induction_on with
  | empty => simp
  | insert _ _ ih =>
    simp only [forall_mem_insert, sUnion_insert] at *
    exact h.1.union (ih h.2)

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