theorem sequence_tendsto_iff_dist_tendsto_zero {X : Type u} [MetricSpace X] {u : ℕ → X} {x : X} : Filter.Tendsto u Filter.atTop (nhds x) ↔ Filter.Tendsto (fun (n : ℕ) => dist (u n) x) Filter.atTop (nhds 0)

In a metric space, a sequence converges to x exactly when its distances to x tend to 0.