no goals
α : Type u
β : Type v
γ : Type ?u.13040
δ : Type ?u.13043
ε : Type ?u.13046
ζ : Type ?u.13049
inst✝ : TopologicalSpace α
S : Set α
x : ↑S
⊢ NeBot (𝓝[{x}ᶜ] x) ↔ NeBot (𝓝[{↑x}ᶜ] ↑x ⊓ 𝓟 S)
rw [neBot_iff, neBot_iff, not_iff_not, nhds_ne_subtype_eq_bot_iff]