English
If a map f from β to α tends to x and also tends to y along a filter l with l nonempty, then the distance between x and y is zero.
Русский
Пусть f: β → α, l — непустой фильтр. Если f стремится к x по l и к y по l, то расстояние между x и y равно нулю.
LaTeX
$$$\\mathrm{Tendsto}\,f\,l\\,(\\mathcal{N}(x)) \\land \\mathrm{Tendsto}\,f\,l\\,(\\mathcal{N}(y)) \\Rightarrow \\operatorname{dist}(x,y)=0$$$
Lean4
/-- A weaker version of `tendsto_nhds_unique` for `PseudoMetricSpace`. -/
theorem tendsto_nhds_unique_dist {f : β → α} {l : Filter β} {x y : α} [NeBot l] (ha : Tendsto f l (𝓝 x))
(hb : Tendsto f l (𝓝 y)) : dist x y = 0 :=
(tendsto_nhds_unique_inseparable ha hb).dist_eq_zero