dense_iInter_of_isOpen — Mathlib

English

A countable intersection of open dense sets is dense.

Русский

Счетное пересечение открытых плотных множеств плотное.

LaTeX

$$$\\\\forall f: \\\\mathbb{N} \\to \\mathrm{Set}(X), \\\\operatorname{IsOpen}(f(n)) \\land \\\\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 type. -/
theorem dense_iInter_of_isOpen [Countable ι] {f : ι → Set X} (ho : ∀ i, IsOpen (f i)) (hd : ∀ i, Dense (f i)) :
    Dense (⋂ s, f s) :=
  dense_sInter_of_isOpen (forall_mem_range.2 ho) (countable_range _) (forall_mem_range.2 hd)

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