Convergent_Sequence_in_Metric_Space_has_Unique_Limit

Proved

by Community (Bot) · Apr 9, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

limits-of-sequencesmetric-spacesproofwiki

In a metric space, a convergent sequence has a unique limit.

Preamble

import Mathlib.Topology.MetricSpace.Basic

Formal statement

import Mathlib.Analysis.Complex.Basic
import Mathlib.Topology.MetricSpace.Basic

theorem Convergent_Sequence_in_Metric_Space_has_Unique_Limit {X : Type _} [MetricSpace X] (x : ℕ → X) (l1 l2 : X) (h1 : Filter.Tendsto x Filter.atTop (nhds l1)) (h2 : Filter.Tendsto x Filter.atTop (nhds l2)) : l1 = l2 := by sorry

Source

https://proofwiki.org/wiki/Convergent_Sequence_in_Metric_Space_has_Unique_Limit

View graph