English
Let X be Hausdorff. For injective-like pairs f,g: Y→X with a, b ∈ X and a nontrivial l, if Tendsto f l (nhds a), Tendsto g l (nhds b), and f =ᶠ[l] g, then a = b.
Русский
Пусть X — хаусдорфово. Для отображений f,g:Y→X, а также пределов a,b и непустого фильтра l, если f сходится по l к a, g сходится по l к b, и f и g совпадают на множество, принадлежащее l, тогда a=b.
LaTeX
$$$\forall X,Y\,[TopologicalSpace\ X]\,[T2Space\ X]\,\forall f,g:Y\to X\,\forall l:\\mathrm{Filter}\ Y\,[l\neq \emptyset],\forall a,b\in X,\Big( Tendsto\ f\ l\ (\\nhds a)\land Tendsto\ g\ l\ (\\nhds b)\Big)\land (f=\!\!\!\mathrm{\text{f}}[l]\ g)\Rightarrow a=b$$$
Lean4
theorem tendsto_nhds_unique_of_eventuallyEq [T2Space X] {f g : Y → X} {l : Filter Y} {a b : X} [NeBot l]
(ha : Tendsto f l (𝓝 a)) (hb : Tendsto g l (𝓝 b)) (hfg : f =ᶠ[l] g) : a = b :=
tendsto_nhds_unique (ha.congr' hfg) hb
