Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)
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 Cauchy sequence in a metric space with a convergent subsequence converges to that subsequence’s 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), let (xk) be a Cauchy sequence in X (Cauchy sequence in a metric space), and suppose some subsequence (xnj) converges to p∈X, that is p is a subsequential limit of (xk) in (X,d) (Convergence of a sequence in a metric space: xk→x iff d(xk,x)→0 in R, Subsequential limit of a real sequence, and the subsequential limit set). Then the whole sequence converges to p.

In particular a Cauchy sequence has at most one subsequential limit, and it has one exactly when it converges.

Facts & Assumptions

Given: A metric space (X,d), a Cauchy sequence (xk) in X, a strictly increasing n:N→N, a point p∈X with xnj→p, and a real ε>0.

[A1]

Cauchyness: for every real η>0 there is K1 with d(xm,xl)<η for all m,l≥K1 (Cauchy sequence in a metric space, The rationals embed densely in the reals).

[A2]

Metric convergence: a sequence (yj) converges to p if and only if for every real η>0 there is K such that d(yj,p)<η for all j≥K. Applied to yj=xnj, the subsequence hypothesis gives K2 with d(xnj,p)<η for all j≥K2 (Convergence of a sequence in a metric space: xk→x iff d(xk,x)→0 in R, The rationals embed densely in the reals).

[L1]

A strictly increasing index map satisfies nj≥j for every j (A strictly increasing index map satisfies nk≥k).

[L3]

Two naturals have a maximum, which is one of them and is at least each of them (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set).

Proof

technique · direct
1.1

Apply [A1] with η=ε/2 to get K1 with d(xm,xl)<ε/2 for all m,l≥K1, and [A2] with η=ε/2 to get K2 with d(xnj,p)<ε/2 for all j≥K2.

A1A2algebra
1.2

Put K:=max⁡{K1,K2}, so K≥K1 and K≥K2.

L3choose
2.1

The index nK satisfies nK≥K≥K1, and K≥K2, so d(xnK,p)<ε/2.

step 1.1step 1.2L1
3.1

Let k≥K. Then k≥K1 and nK≥K1, so d(xk,xnK)<ε/2, and therefore d(xk,p)≤d(xk,xnK)+d(xnK,p)<ε/2+ε/2=ε.

step 1.1step 1.2step 2.1L1L2algebra
4.1

Since ε>0 was an arbitrary real, xk→p in (X,d).

step 3.1A2∎

Remarks

  • Where nj≥j is used. In step 2.1, and quoted again in step 3.1, and both places matter: it puts the single chosen subsequence term xnK beyond the Cauchy index K1, and it is what lets one index K control the subsequence and the sequence at once. Without it the subsequence could in principle look only at small indices, and the Cauchy hypothesis would never be reached.
  • Only one term of the subsequence is used. The proof does not pass to the limit along the subsequence; it fixes the single index nK and routes every later term of the whole sequence through it. That is why no further hypothesis on the subsequence is needed.
  • This is the lemma that turns compactness into completeness. A space in which every sequence has a convergent subsequence is complete (Complete metric space: every Cauchy sequence converges in the space) by this lemma alone, applied to a Cauchy sequence. The converse is false, not merely harder: R is complete (R and Rn for n≥1 with the Euclidean metric are complete, componentwise from the Cauchy criterion in R) and the sequence xk=k has no convergent subsequence, its terms being at pairwise distance at least 1 so that no subsequence is Cauchy. What does hold is that a complete space in which every sequence has a convergent subsequence is exactly a complete and totally bounded one, and total boundedness is a later page of this library.

Depends on

Used by

Dependency tree · two levels

31 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