LemmaStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)verified 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.

Every convergent sequence in a metric space is Cauchy

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$ converging to $p \in X$ (Convergence of a sequence in a metric space: $x_k \to x$ iff $d(x_k, x) \to 0$ in $\mathbb{R}$ ). Then $(x_k)$ is Cauchy in $(X,d)$ (Cauchy sequence in a metric space).

The converse fails, and that failure is the subject of this page (FALSE: every Cauchy sequence in a metric space converges).

Facts & Assumptions

Given: A metric space $(X,d)$ , a sequence $(x_k)$ in $X$ , a point $p \in X$ with $x_k \to p$ , and a real $\varepsilon > 0$ .

[A1]

Convergence: for every real $\eta > 0$ there is $K \in \mathbb{N}$ with $d(x_k,p) < \eta$ for all $k \ge K$ (Convergence of a sequence in a metric space: $x_k \to x$ iff $d(x_k, x) \to 0$ in $\mathbb{R}$ , Limits and Cauchy sequences of reals, The rationals embed densely in the reals).

[A2]

Cauchyness is established by producing, for every real $\varepsilon > 0$ , an index $K$ with $d(x_m,x_n) < \varepsilon$ for all $m,n \ge K$ (Cauchy sequence in a metric space, The rationals embed densely in the reals).

[L1]

Triangle inequality (M3) and symmetry (M2) of a metric (Metric space: $d(x,y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric).

Proof

technique · direct

1.1

The real $\varepsilon/2$ is positive, so [A1] applied with $\eta = \varepsilon/2$ supplies $K \in \mathbb{N}$ with $d(x_k, p) < \varepsilon/2$ for every $k \ge K$ .

A1algebra

1.2

For all $m, n \in \mathbb{N}$ one has $d(x_m, x_n) \le d(x_m, p) + d(p, x_n)$ .

2.1

Hence for all $m, n \ge K$ : $d(x_m,x_n) \le d(x_m,p) + d(p,x_n) < \varepsilon/2 + \varepsilon/2 = \varepsilon$ .

step 1.1step 1.2algebra

3.1

Since $\varepsilon > 0$ was an arbitrary real, $(x_k)$ is Cauchy in $(X,d)$ .

step 2.1A2∎

Remarks

The proof spends the triangle inequality and symmetry, but not separation. Symmetry rewrites $d(p,x_n)$ as the bounded quantity $d(x_n,p)$ in step 2.1. The separation axiom (M1) is not used, so the same argument shows that a sequence converging in a pseudometric space (Metric space: $d(x,y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric) is Cauchy for the pseudometric.
Halving is the whole idea. The Cauchy condition compares two terms of the sequence, and a limit compares one term with the limit; routing $m$ and $n$ through $p$ costs two applications of the convergence hypothesis, so each is run at half the target. Every proof on this page that produces a Cauchy sequence out of a convergent one repeats this step.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 59 results over 26 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Cauchy sequence (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 3 (standard reference, not scraped)