no goals
α : Type u
β : Type v
γ : Type ?u.12421
δ : Type ?u.12424
ε : Type ?u.12427
ζ : Type ?u.12430
inst✝ : TopologicalSpace α
S : Set α
x : ↑S
⊢ 𝓝[{x}ᶜ] x = ⊥ ↔ 𝓝[{↑x}ᶜ] ↑x ⊓ 𝓟 S = ⊥
rw [← nhdsWithin_subtype_eq_bot_iff, preimage_compl, ← image_singleton,
  Subtype.coe_injective.preimage_image]