no goals
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set (Set α)
⊢ (∀ (t : Set α), t ∈ s → IsClosed t) → IsClosed (⋂₀ s)
simpa only [← isOpen_compl_iff, compl_sInter, sUnion_image] using isOpen_biUnion