union — Mathlib

English

The union of two Gδ sets is a Gδ set.

Русский

Объединение двух Gδ множеств является Gδ.

LaTeX

$$$IsGδ(s) \\land IsGδ(t) \\Rightarrow IsGδ(s \\cup t)$$$

Lean4

/-- The union of two Gδ sets is a Gδ set. -/
theorem union {s t : Set X} (hs : IsGδ s) (ht : IsGδ t) : IsGδ (s ∪ t) :=
  by
  rcases hs with ⟨S, Sopen, Scount, rfl⟩
  rcases ht with ⟨T, Topen, Tcount, rfl⟩
  rw [sInter_union_sInter]
  refine .biInter_of_isOpen (Scount.prod Tcount) ?_
  rintro ⟨a, b⟩ ⟨ha, hb⟩
  exact (Sopen a ha).union (Topen b hb)

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