no goals
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
x : α
F : Filter α
⊢ AccPt x F ↔ ClusterPt x (𝓟 ({x}ᶜ) ⊓ F)
rw [AccPt, nhdsWithin, ClusterPt, inf_assoc]