English
If nhdsWithin x t and s and t are related by eventual equality, then nhds x of insert x s equals nhds x of insert x t.
Русский
Если nhdsWithin x t и s эквивалентны в смысле eventually, то nhds x (insert x s) эквивалентно nhds x (insert x t).
LaTeX
$$$s =_{nhdsWithin[x] } t \Rightarrow (insert x s) =_{nhds} (insert x t).$$$
Lean4
theorem eventuallyEq_insert [T1Space X] {s t : Set X} {x y : X} (h : s =ᶠ[𝓝[{ y }ᶜ] x] t) :
(insert x s : Set X) =ᶠ[𝓝 x] (insert x t : Set X) :=
by
simp_rw [eventuallyEq_set] at h ⊢
simp_rw [← union_singleton, ← nhdsWithin_univ, ← compl_union_self { x }, nhdsWithin_union, eventually_sup,
nhdsWithin_singleton, eventually_pure, union_singleton, mem_insert_iff, true_or, and_true]
filter_upwards [nhdsWithin_compl_singleton_le x y h] with y using or_congr (Iff.rfl)
