English
The intersection of two dense Gδ sets is dense.
Русский
Пересечение плотных Gδ-множеств остаётся плотным.
LaTeX
$$$\\\\forall s,t \\\\ IsGδ(s) \\\\land IsGδ(t) \\\\land Dense(s) \\\\land Dense(t) \\\\Rightarrow Dense(s \\cap t)$$$
Lean4
/-- Baire theorem: the intersection of two dense Gδ sets is dense. -/
theorem inter_of_Gδ {s t : Set X} (hs : IsGδ s) (ht : IsGδ t) (hsc : Dense s) (htc : Dense t) : Dense (s ∩ t) :=
by
rw [inter_eq_iInter]
apply dense_iInter_of_Gδ <;> simp [Bool.forall_bool, *]