tendsto_nhds_unique_dist — Mathlib

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

Похожие утверждения