English
A countable family of dense Gδ sets has a dense intersection.
Русский
Счетное семейство плотных Gδ-множестv имеет плотное пересечение.
LaTeX
$$$\\\\forall S \\\\subseteq \\text{Set}(α), \\\\text{IsGδ}(S) \\\\Rightarrow \\\\operatorname{Dense}(\\\\bigcap S)$$$
Lean4
/-- Baire theorem: a countable intersection of dense Gδ sets is dense. Formulated here with
an index set which is a countable set in any type. -/
theorem dense_biInter_of_Gδ {S : Set α} {f : ∀ x ∈ S, Set X} (ho : ∀ s (H : s ∈ S), IsGδ (f s H)) (hS : S.Countable)
(hd : ∀ s (H : s ∈ S), Dense (f s H)) : Dense (⋂ s ∈ S, f s ‹_›) :=
by
rw [biInter_eq_iInter]
haveI := hS.to_subtype
exact dense_iInter_of_Gδ (fun s => ho s s.2) fun s => hd s s.2
