English
Let X be a Hausdorff space. If a function f: Y → X has a filter l on Y that is nontrivial, and f l-converges to a and also to b in X, then a = b.
Русский
Пусть X — хаусдорфово пространство. Если функция f: Y → X имеет фильтр l на Y, не тождественный нулю, и f сходится по l к a и к b в X, то a = b.
LaTeX
$$$\forall X,Y\,[TopologicalSpace\ X]\,[T2Space\ X]\,\forall f:Y\to X\,\forall l:\\mathrm{Filter}\ Y\,[l\neq \emptyset],\forall a,b\in X,\\Big(\,Tendsto\ f\ l\ (\\nhds a)\land Tendsto\ f\ l\ (\\nhds b)\Big)\Rightarrow a=b$$$
Lean4
theorem tendsto_nhds_unique [T2Space X] {f : Y → X} {l : Filter Y} {a b : X} [NeBot l] (ha : Tendsto f l (𝓝 a))
(hb : Tendsto f l (𝓝 b)) : a = b :=
(tendsto_nhds_unique_inseparable ha hb).eq
