iInter — Mathlib

English

The intersection of a countable family of Gδ sets is Gδ.

Русский

Пересечение счетной семейности Gδ множеств является Gδ.

LaTeX

$$$\\forall i, IsGδ(s(i))\\Rightarrow IsGδ(\\bigcap_i s(i))$$$

Lean4

/-- The intersection of an encodable family of Gδ sets is a Gδ set. -/
protected theorem iInter [Countable ι'] {s : ι' → Set X} (hs : ∀ i, IsGδ (s i)) : IsGδ (⋂ i, s i) :=
  by
  choose T hTo hTc hTs using hs
  obtain rfl : s = fun i => ⋂₀ T i := funext hTs
  refine ⟨⋃ i, T i, ?_, countable_iUnion hTc, (sInter_iUnion _).symm⟩
  simpa [@forall_swap ι'] using hTo

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