Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-26 (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 has at most one limit

Statement

Let (xk) be a sequence of reals (Sequences of reals: bounded, eventually, frequently, tails, subsequences) and let x,y∈R. If (xk) converges to x and (xk) converges to y (Limits and Cauchy sequences of reals), then x=y. A sequence therefore has at most one limit, and when a limit exists it may be denoted lim⁡kxk.

Facts & Assumptions

Given: A sequence (xk) of reals and reals x,y such that (xk) converges to x and (xk) converges to y (Sequences of reals: bounded, eventually, frequently, tails, subsequences, Limits and Cauchy sequences of reals).

[L1]

Convergence: (xk) converges to z when for every rational ε>0 there is K∈N with ∣xk−z∣<ε for all k≥K (Limits and Cauchy sequences of reals).

[L2]

Triangle inequality: ∣a+b∣≤∣a∣+∣b∣ in any ordered field, in particular in R (The triangle inequality, Complete ordered field (least-upper-bound property)).

[L3]

Absolute value: ∣u∣≥0, and ∣u∣=0 if and only if u=0, and ∣−u∣=∣u∣ (Basic properties of the absolute value).

[L4]

Small rationals: for every real η>0 there is a rational ε with 0<ε<η. Either route gives this: density of Q in R (The rationals embed densely in the reals) applied to the pair 0<η; or the Archimedean property (Every complete ordered field is Archimedean) applied to 1/η, which yields a natural n≥1 with 1/η<n and hence 0<1/n<η (Inverses of positives are positive, and reciprocation reverses order).

[L5]

Order arithmetic in R. Trichotomy, so u≠0 together with ∣u∣≥0 and ∣u∣≠0 forces ∣u∣>0; transitivity and irreflexivity of <; and, since u≤v means u<v or u=v, the mixed form u≤v<w⇒u<w (Complete ordered field (least-upper-bound property), Ordered field). Adding two strict inequalities: a<b and c<d give a+c<b+d (Order is preserved by adding a constant and by adding inequalities). Multiplying by a positive: for c>0, a<b gives ac<bc (Sign rules for products and monotonicity of multiplication). Halving a positive: 1>0 (The multiplicative identity is positive), so 2:=1+1>0 because the positives are closed under addition (Ordered field), hence 2−1>0 (Inverses of positives are positive, and reciprocation reverses order) and η/2=η⋅2−1>0 whenever η>0 (Sign rules for products and monotonicity of multiplication).

[L6]

The order on N is total, so any two indices K1,K2 admit an index k with k≥K1 and k≥K2 (≤ is a linear order on N).

Proof

technique · contradiction
1.1

Suppose, for contradiction, that x≠y.

assume-contra
2.1

Then x−y≠0, so ∣x−y∣≠0 while ∣x−y∣≥0; by trichotomy ∣x−y∣>0, and hence ∣x−y∣/2>0.

step 1.1L3L5
3.1

Choose a rational ε with 0<ε<∣x−y∣/2; multiplying that inequality by 2>0 and using (∣x−y∣/2)⋅2=∣x−y∣ gives 2ε<∣x−y∣.

step 2.1L4L5algebrachoose
4.1

Since (xk) converges to x there is K1 with ∣xk−x∣<ε for all k≥K1, and since (xk) converges to y there is K2 with ∣xk−y∣<ε for all k≥K2.

step 3.1L1
5.1

Fix an index k with k≥K1 and k≥K2; then ∣x−y∣=∣(x−xk)+(xk−y)∣≤∣x−xk∣+∣xk−y∣=∣xk−x∣+∣xk−y∣, while adding the two strict inequalities of step 4.1 gives ∣xk−x∣+∣xk−y∣<ε+ε=2ε; composing the non-strict inequality with the strict one yields ∣x−y∣<2ε.

step 4.1L2L3L5L6
6.1

Combining, 2ε<∣x−y∣<2ε, so 2ε<2ε, which contradicts irreflexivity of the strict order.

step 3.1step 5.1L5
7.1

The assumption x≠y is therefore untenable, so x=y: a sequence of reals has at most one limit.

step 6.1discharge-contradiction∎

Remarks

  • Uniqueness is what licenses the notation lim⁡kxk and the phrase the limit. Without it the symbol would not denote. This library writes lim⁡kxk only for sequences already known to converge, exactly as it writes sup⁡S only for sets already known to have a supremum (Conventions: sup⁡∅, unbounded sets, and the extended reals).

  • The proof uses only that R is an ordered field in which arbitrarily small positive rationals exist, that is, an Archimedean ordered field (Every complete ordered field is Archimedean). Completeness is not needed: limits are unique in Q too, where many sequences fail to have one.

  • The hypothesis is genuinely about a single sequence having two limits. Two different sequences may of course share a limit, and a sequence with no limit at all is not excluded by anything here.

Depends on

Used by

Dependency tree · two levels

36 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources