English
If ι is countable, and f(i) are Gδ and dense, then their intersection is dense.
Русский
Если множество индексов ι счетно, и для каждого i множество f(i) является Gδ и плотным, то их пересечение плотное.
LaTeX
$$$\\\\forall i \\\\in ι, \\\\operatorname{IsGδ}(f(i)) \\\\land \\\\operatorname{Dense}(f(i)) \\\\Rightarrow \\\\operatorname{Dense}(\\\\bigcap_{i} f(i))$$$
Lean4
/-- Baire theorem: a countable intersection of dense Gδ sets is dense. Formulated here with
an index set which is a countable type. -/
theorem dense_iInter_of_Gδ [Countable ι] {f : ι → Set X} (ho : ∀ s, IsGδ (f s)) (hd : ∀ s, Dense (f s)) :
Dense (⋂ s, f s) :=
dense_sInter_of_Gδ (forall_mem_range.2 ‹_›) (countable_range _) (forall_mem_range.2 ‹_›)
