English
In a T1 space, if x ≠ y, then nhdsWithin(insert y s) at x equals nhdsWithin(s) at x.
Русский
В T1-пространстве, если x ≠ y, то nhdsWithin (insert y s) в точке x равен nhdsWithin s в x.
LaTeX
$$$\\text{If } [T1Space X], x \\neq y, \\; \\mathcal{N}_{[\\mathrm{insert}\\; y\\; s]}(x) = \\mathcal{N}_{s}(x).$$$
Lean4
theorem nhdsWithin_insert_of_ne [T1Space X] {x y : X} {s : Set X} (hxy : x ≠ y) : 𝓝[insert y s] x = 𝓝[s] x :=
by
refine le_antisymm (Filter.le_def.2 fun t ht => ?_) (nhdsWithin_mono x <| subset_insert y s)
obtain ⟨o, ho, hxo, host⟩ := mem_nhdsWithin.mp ht
refine mem_nhdsWithin.mpr ⟨o \ { y }, ho.sdiff isClosed_singleton, ⟨hxo, hxy⟩, ?_⟩
rw [inter_insert_of_notMem <| notMem_diff_of_mem (mem_singleton y)]
exact (inter_subset_inter diff_subset Subset.rfl).trans host
