English
A countable family of open dense sets has a dense intersection.
Русский
Счетное семейство открытых плотных множеств имеет плотное пересечение.
LaTeX
$$$\\\\forall f: ι \\to Set(X), (\\\\forall i, IsOpen(f(i))) \\\\land (\\\\forall i, Dense(f(i))) \\\\Rightarrow Dense(\\\\bigcap_{i} f(i))$$$
Lean4
/-- If a countable family of closed sets cover a dense `Gδ` set, then the union of their interiors
is dense. Formulated here with a union over a countable set in any type. -/
theorem dense_biUnion_interior_of_closed {t : Set α} {s : Set X} (hs : IsGδ s) (hd : Dense s) (ht : t.Countable)
{f : α → Set X} (hc : ∀ i ∈ t, IsClosed (f i)) (hU : s ⊆ ⋃ i ∈ t, f i) : Dense (⋃ i ∈ t, interior (f i)) :=
by
haveI := ht.to_subtype
simp only [biUnion_eq_iUnion, SetCoe.forall'] at *
exact hs.dense_iUnion_interior_of_closed hd hc hU
