no goals
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ closure s ⊆ s ↔ ∀ (a : α), ClusterPt a (𝓟 s) → a ∈ s
simp only [subset_def, mem_closure_iff_clusterPt]