α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
x y : α
h : x ≠ y
s : Set α
⊢ {y}ᶜ ∈ 𝓝[s] x
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
x y : α
h : x ≠ y
s : Set α
⊢ 𝓝[s \ {y}] x = 𝓝[s] x
rw [diff_eq, inter_comm, nhdsWithin_inter_of_mem]
no goals
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
x y : α
h : x ≠ y
s : Set α
⊢ {y}ᶜ ∈ 𝓝[s] x
exact mem_nhdsWithin_of_mem_nhds (isOpen_ne.mem_nhds h)