no goals
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Set α
hs : Set.Subsingleton s
⊢ Set.Subsingleton (_root_.closure s)
rcases hs.eq_empty_or_singleton with (rfl | ⟨x, rfl⟩) <;> simp