English
A countable intersection of open dense sets is dense.
Русский
Счетное пересечение открытых плотных множеств плотное.
LaTeX
$$$\\\\forall f: \\\\mathbb{N} \\to \\mathrm{Set}(X), \\\\operatorname{IsOpen}(f(n)) \\text{ и } \\\\operatorname{Dense}(f(n)) \\\\Rightarrow \\\\operatorname{Dense}(\\\\bigcap_{n} f(n))$$$
Lean4
/-- Baire theorem: a countable intersection of dense open sets is dense. Formulated here with
an index set which is a countable set in any type. -/
theorem dense_biInter_of_isOpen {S : Set α} {f : α → Set X} (ho : ∀ s ∈ S, IsOpen (f s)) (hS : S.Countable)
(hd : ∀ s ∈ S, Dense (f s)) : Dense (⋂ s ∈ S, f s) :=
by
rw [← sInter_image]
refine dense_sInter_of_isOpen ?_ (hS.image _) ?_ <;> rwa [forall_mem_image]
