α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Set α
hs : Set.Finite s
⊢ IsClosed (⋃ (x : α) (_ : x ∈ s), {x})
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Set α
hs : Set.Finite s
⊢ IsClosed s
rw [← biUnion_of_singleton s]
no goals
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Set α
hs : Set.Finite s
⊢ IsClosed (⋃ (x : α) (_ : x ∈ s), {x})
exact isClosed_biUnion hs fun i _ => isClosed_singleton