no goals
α : Type u_1
β : Type ?u.1018
γ : Type ?u.1021
δ : Type ?u.1024
inst✝ : TopologicalSpace α
z : α
s : Set α
⊢ z ∈ closure (s \ {z}) ↔ ∃ᶠ (x : α) in 𝓝[{z}ᶜ] z, x ∈ s
simp [mem_closure_iff_frequently, frequently_nhdsWithin_iff]