LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-08-02 (claude-opus-5)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A sequence in a metric space has at most one limit

Statement

Let $(X, d)$ be a metric space (Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric) and let $(x_{k})$ be a sequence in $X$ (Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ ). If $x_{k} \to p$ and $x_{k} \to q$ , then $p = q$ .

So a convergent sequence in a metric space has exactly one limit, and the notation $\lim_{k} x_{k}$ is unambiguous.

Facts & Assumptions

Given: A metric space $(X, d)$ , a sequence $(x_{k})$ in $X$ , and points $p, q \in X$ with $x_{k} \to p$ and $x_{k} \to q$ .

[A1]

Convergence: $x_{k} \to p$ means that for every rational $ε > 0$ there is $K \in N$ with $d (x_{k}, p) < ε$ for all $k \geq K$ (Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ , Limits and Cauchy sequences of reals); and $d (x, y) \geq 0$ for all $x, y \in X$ , so in particular $d (x_{k}, p) \geq 0$ and its absolute value is itself (Nonnegativity of a metric is a consequence of the other axioms, not an axiom, Absolute value in an ordered field, Basic properties of the absolute value).

[L1]

Density of the rationals: strictly between any two reals lies a rational, so below any real $η > 0$ there is a rational $ε$ with $0 < ε < η$ (The rationals embed densely in the reals).

[L2]

Halving. For a real $c > 0$ set $2 : = 1 + 1$ and $c / 2 : = c \cdot 2^{- 1}$ . Then $2 > 0$ , so $2 \neq 0$ and $2^{- 1} > 0$ (The multiplicative identity is positive, Order is preserved by adding a constant and by adding inequalities, Inverses of positives are positive, and reciprocation reverses order, Ordered field); hence $c / 2 > 0$ (Sign rules for products and monotonicity of multiplication); and $c / 2 + c / 2 = c (2^{- 1} + 2^{- 1}) = c (2 \cdot 2^{- 1}) = c$ (Field).

[L3]

Separation (M1) and the triangle inequality (M3) of $d$ , together with symmetry (M2) (Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric).

[L4]

Trichotomy of the order of $R$ , and transitivity: $a < b$ and $b \leq a$ cannot both hold (Complete ordered field (least-upper-bound property), Ordered field).

[L5]

Adding two inequalities: $a < b$ and $c < d$ give $a + c < b + d$ (Order is preserved by adding a constant and by adding inequalities).

Proof

technique · contradiction

1.1assume-contra

Suppose, for contradiction, that $p \neq q$ .

2.1step 1.1A1L2L3L4

By (M1) $d (p, q) \neq 0$ , and $d (p, q) \geq 0$ , so $c : = d (p, q) > 0$ by trichotomy; put $η : = c / 2$ , a positive real with $η + η = c$ .

3.1step 2.1A1L1choose

Fix a rational $ε$ with $0 < ε < η$ , and use the convergence hypotheses at $ε$ to fix $K_{1}, K_{2} \in N$ with $d (x_{k}, p) < ε$ for $k \geq K_{1}$ and $d (x_{k}, q) < ε$ for $k \geq K_{2}$ .

4.1step 3.1choose

Let $m$ be any natural with $m \geq K_{1}$ and $m \geq K_{2}$ , for instance $m : = K_{1} + K_{2}$ ; then $d (x_{m}, p) < ε$ and $d (x_{m}, q) < ε$ .

5.1step 4.1step 2.1L3L5

By symmetry and the triangle inequality, $c = d (p, q) \leq d (p, x_{m}) + d (x_{m}, q) = d (x_{m}, p) + d (x_{m}, q) < ε + ε < η + η = c$ .

6.1step 5.1L4discharge-contradiction∎

Step 5.1 asserts $c < c$ , which trichotomy forbids; the supposition of step 1.1 is therefore untenable and $p = q$ .

Remarks

Where each axiom is spent. Separation (M1) is what turns $p \neq q$ into $d (p, q) > 0$ , and it is the only axiom that distinguishes a metric from a pseudometric (Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric). In a pseudometric space with $d (p, q) = 0$ and $p \neq q$ , the constant sequence $x_{k} = p$ converges to both, so the lemma is false there and this is exactly the step that fails.
The same argument proves more, namely that a metric space is Hausdorff: the balls $B (p, c / 2)$ and $B (q, c / 2)$ are disjoint. That is recorded separately as Distinct points of a metric space have disjoint balls around them, and uniqueness of limits follows from it as well.
Instantiating at a rational is not cosmetic. Limits and Cauchy sequences of reals quantifies over rational $ε$ , so a convergence hypothesis may only be applied at a rational; step 3.1 passes from the real $η$ to a rational below it using The rationals embed densely in the reals, which is the sanctioned move.

A sequence in a metric space has at most one limit

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources