no goals
ι : Type u_1
ι' : Type ?u.8039
α : Type ?u.8042
X : Type u_2
Y : Type ?u.8048
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed (f i)
⊢ IsClosed (⋃ (i : ι), f i)
simp only [← closure_eq_iff_isClosed, hf.closure_iUnion, (hc _).closure_eq]