English
Let X be Hausdorff. If f,g:Y→X with a,b∈X and l a nontrivial filter on Y satisfy Tendsto f l (nhds a), Tendsto g l (nhds b), and f and g agree frequently along l, then a=b.
Русский
Пусть X — хаусдорфово. Если f,g:Y→X удовлетворяют условиям сходящности по l к a и b соответственно, и они часто совпадают по 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 \big(\exists\!\text{ or }\exists^\!\!\text{f} x\in l:\ f x=g x\big)\Rightarrow a=b$$$
Lean4
theorem tendsto_nhds_unique_of_frequently_eq [T2Space X] {f g : Y → X} {l : Filter Y} {a b : X} (ha : Tendsto f l (𝓝 a))
(hb : Tendsto g l (𝓝 b)) (hfg : ∃ᶠ x in l, f x = g x) : a = b :=
have : ∃ᶠ z : X × X in 𝓝 (a, b), z.1 = z.2 := (ha.prodMk_nhds hb).frequently hfg
not_not.1 fun hne => this (isClosed_diagonal.isOpen_compl.mem_nhds hne)
