dense_iInter_of_isOpen_nat — Mathlib

English

A Baire space property: a countable intersection of open dense sets is dense.

Русский

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

LaTeX

$$$\\\\forall f: \\mathbb{N} \\to \\mathrm{Set}(X), \\\\big( \\forall n, \\\\operatorname{IsOpen}(f(n)) \\big) \\\\land \\\\big( \\forall n, \\\\operatorname{Dense}(f(n)) \\big) \\\\Rightarrow \\\\operatorname{Dense}(\\\\bigcap_{n} f(n))$$$

Lean4

/-- Definition of a Baire space. -/
theorem dense_iInter_of_isOpen_nat {f : ℕ → Set X} (ho : ∀ n, IsOpen (f n)) (hd : ∀ n, Dense (f n)) :
    Dense (⋂ n, f n) :=
  BaireSpace.baire_property f ho hd

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