English
A countable collection of open dense sets indexed by a countable set has a dense intersection.
Русский
Счетное множество открытых плотных множеств имеет плотное пересечение.
LaTeX
$$$\\text{Dense}(\\\\bigcap_{s \\in S} s)$, где каждый s \\in S открыт и плотен и S счетно.$$
Lean4
/-- Baire theorem: a countable intersection of dense open sets is dense. Formulated here with ⋂₀. -/
theorem dense_sInter_of_isOpen {S : Set (Set X)} (ho : ∀ s ∈ S, IsOpen s) (hS : S.Countable) (hd : ∀ s ∈ S, Dense s) :
Dense (⋂₀ S) := by
rcases S.eq_empty_or_nonempty with h | h
· simp [h]
· rcases hS.exists_eq_range h with ⟨f, rfl⟩
exact dense_iInter_of_isOpen_nat (forall_mem_range.1 ho) (forall_mem_range.1 hd)
