dense_sInter_of_Gδ — Mathlib

English

The intersection of two dense Gδ sets is dense.

Русский

Пересечение двух плотных Gδ-множестv плотное.

LaTeX

$$$\\\\operatorname{IsGδ}(s) \\\\land \\\\operatorname{IsGδ}(t) \\\\land \\\\operatorname{Dense}(s) \\\\land \\\\operatorname{Dense}(t) \\\\Rightarrow \\\\operatorname{Dense}(s \\cap t)$$$

Lean4

/-- Baire theorem: a countable intersection of dense Gδ sets is dense. Formulated here with ⋂₀. -/
theorem dense_sInter_of_Gδ {S : Set (Set X)} (ho : ∀ s ∈ S, IsGδ s) (hS : S.Countable) (hd : ∀ s ∈ S, Dense s) :
    Dense (⋂₀ S) :=
  dense_of_mem_residual ((countable_sInter_mem hS).mpr (fun _ hs => residual_of_dense_Gδ (ho _ hs) (hd _ hs)))

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