no goals
α : Type u_1
β : Type u_2
γ : Type ?u.29633
ι : Type ?u.29636
inst✝³ : TopologicalSpace α
inst✝² : BaireSpace α
inst✝¹ : Nonempty α
inst✝ : Encodable β
f : β → Set α
hc : ∀ (s : β), IsClosed (f s)
hU : (⋃ (s : β), f s) = univ
⊢ ∃ s, Set.Nonempty (interior (f s))
simpa using (dense_iUnion_interior_of_closed hc hU).nonempty