English
A countable family of closed sets covering a dense Gδ set yields that the union of their interiors is dense.
Русский
Счетное семейство замкнутых множеств, покрывающих плотное множество Gδ, порождает плотность объединения внутренних множеств.
LaTeX
$$$$IsGδ(s) \\\\land Dense(s) \\\\Rightarrow Dense(\\\\bigcup t \\\\operatorname{interior}(t))$$$$
Lean4
/-- If a countable family of closed sets cover a dense `Gδ` set, then the union of their interiors
is dense. Formulated here with `⋃₀`. -/
theorem dense_sUnion_interior_of_closed {T : Set (Set X)} {s : Set X} (hs : IsGδ s) (hd : Dense s) (hc : T.Countable)
(hc' : ∀ t ∈ T, IsClosed t) (hU : s ⊆ ⋃₀ T) : Dense (⋃ t ∈ T, interior t) :=
hs.dense_biUnion_interior_of_closed hd hc hc' <| by rwa [← sUnion_eq_biUnion]
