02.03.02 · analysis / sequences-series

Cauchy sequences and Bolzano-Weierstrass

shipped3 tiersLean: partial

Anchor (Master): Bolzano 1817 *Rein analytischer Beweis des Lehrsatzes* (originator of the bounded-set-clustering lemma); Weierstrass 1860s Berlin lectures (published 1885); Cauchy 1821 *Cours d'analyse* (originator of the Cauchy criterion); Apostol *Calculus* Vol. 1 Ch. 10; Bourbaki *Topologie Générale* Ch. II §3

Intuition [Beginner]

A sequence is an infinite list of real numbers $a_{1}, a_{2}, a_{3}, \dots$ , one for every counting number. Two questions matter most. First: do the numbers in the list eventually settle down to a single target? Second: even if the whole list does not settle, can we pick out a sub-list of terms that does?

The first question is the question of convergence. The second is the question of subsequence existence. The pair of theorems in this unit answers both for real-number sequences and ties the two answers together.

The Cauchy criterion answers convergence from the inside. Instead of naming the target in advance, it asks whether the later terms of the list get arbitrarily close to each other. If they do — if every pair of late terms eventually fits inside a tiny window — the sequence converges, and the target it converges to is automatically a real number. No target needs to be guessed.

The Bolzano-Weierstrass theorem answers subsequence existence by a simple bounded-list rule. If every term of the list lies inside a fixed interval like $[- 10, 10]$ , then no matter how erratically the terms jump around, some pattern of choices through the list picks out a sub-list that homes in on a single real number. Boundedness alone is enough to guarantee a convergent sub-list.

Together the two theorems say: in the real line, a list converges exactly when its later terms cluster against each other, and a bounded list always contains a sub-list that converges. These rules are what let calculus turn boundedness into limits and limits into computations.

Visual [Beginner]

The figure has two parts. The top is a number line with sequence terms placed on it, with the early terms scattered and the later terms packed tighter and tighter around a single marked point. The bottom is a bounded interval being cut in half repeatedly: at each step one half contains infinitely many terms of the sequence and is shaded; the shaded halves shrink down to a single point on the line.

The top picture is the Cauchy criterion in cartoon form: late terms huddle together. The bottom picture is the Bolzano-Weierstrass construction: a bounded sequence, no matter how it jumps, must have an infinitely populated half at every bisection step, and the shrinking shaded halves trap a single real-number target.

Worked example [Beginner]

Take the specific sequence $a_{n} = (- 1)^{n} / n$ , whose first ten terms are $- 1, 1/2, - 1/3, 1/4, - 1/5, 1/6, - 1/7, 1/8, - 1/9, 1/10$ . Every term lies between $- 1$ and $1$ , so the sequence is bounded.

Pick the even-indexed terms: $a_{2} = 1/2$ , $a_{4} = 1/4$ , $a_{6} = 1/6$ , $a_{8} = 1/8$ . These are all positive and they shrink toward $0$ — that is a sub-list that converges to $0$ . Pick the odd-indexed terms: $a_{1} = - 1$ , $a_{3} = - 1/3$ , $a_{5} = - 1/5$ . These are all negative and they also shrink toward $0$ . So both natural sub-lists converge to $0$ , and Bolzano-Weierstrass is delivering one of them as the guaranteed convergent sub-list.

The full sequence happens to converge to $0$ as well, since every term has size at most $1/ n$ and $1/ n$ shrinks to $0$ . To see the Cauchy criterion in action, take any small window — say width $0.001$ . Once $n$ is at least $1000$ , every term $a_{n}$ has size at most $1/1000 = 0.001$ , so any two terms from index $1000$ onward differ by at most $0.002$ . That is the Cauchy condition meeting its bound.

What this tells us: even a sequence that jumps signs forever can be both Cauchy and convergent, and a bounded sequence always serves up a convergent sub-list — here, the even-index one — for free.

Check your understanding [Beginner]

Formal definition [Intermediate+]

Fix the real line $R$ with its absolute value and the usual order from 02.02.01. A sequence in $R$ is a function $a : N \to R$ , written $(a_{n})_{n \geq 1}$ or simply $(a_{n})$ .

Definition (Cauchy sequence). A sequence $(a_{n})$ in $R$ is Cauchy iff for every $ε > 0$ there exists $N \in N$ such that $m, n \geq N$ implies $∣ a_{m} - a_{n} ∣ < ε$ .

Definition (bounded sequence). A sequence $(a_{n})$ is bounded iff there exists $M > 0$ such that $∣ a_{n} ∣ \leq M$ for all $n \in N$ .

Definition (subsequence). A subsequence of $(a_{n})$ is a sequence of the form $(a_{n_{k}})_{k \geq 1}$ , where $n_{1} < n_{2} < n_{3} < \dots$ is a strictly increasing sequence of indices in $N$ . Formally, $k \mapsto n_{k}$ is a strictly increasing function $N \to N$ .

Definition (convergence). $(a_{n})$ converges to $L \in R$ iff for every $ε > 0$ there exists $N \in N$ such that $n \geq N$ implies $∣ a_{n} - L ∣ < ε$ . Write $a_{n} \to L$ or $lim_{n \to \infty} a_{n} = L$ .

The presentation follows Apostol ^{[Apostol Ch. 10 §10.7]} and Rudin ^{[Rudin Ch. 3]}; both organise the chapter so that the Cauchy criterion follows boundedness and precedes Bolzano-Weierstrass.

Counterexamples to common slips

Cauchy is not the same as "consecutive differences shrink". The harmonic sequence $a_{n} = 1 + 1/2 + 1/3 + \dots + 1/ n$ has $∣ a_{n + 1} - a_{n} ∣ = 1/ (n + 1) \to 0$ , yet $(a_{n})$ is not Cauchy: the gap $∣ a_{2 n} - a_{n} ∣$ exceeds $1/2$ for every $n$ . The Cauchy condition controls all pairs $m, n \geq N$ , not just adjacent ones.
Bolzano-Weierstrass needs boundedness. The sequence $a_{n} = n$ has no convergent subsequence — every subsequence is unbounded. Drop the boundedness hypothesis and the theorem fails.
A convergent subsequence does not force convergence of the full sequence. $a_{n} = (- 1)^{n}$ has subsequences converging to $+ 1$ and to $- 1$ ; the full sequence converges to neither.
The rationals fail the Cauchy criterion. The sequence of rational truncations of $2$ — $1, 1.4, 1.41, 1.414, \dots$ — is Cauchy in $Q$ but has no rational limit. The Cauchy criterion's equivalence with convergence is a statement about $R$ , not about ordered fields in general.

Key theorem with proof [Intermediate+]

Theorem (Bolzano-Weierstrass). Every bounded sequence $(a_{n})$ in $R$ has a convergent subsequence.

Proof. Let $M > 0$ satisfy $∣ a_{n} ∣ \leq M$ for every $n$ , so every term lies in the closed interval $I_{0} = [- M, M]$ . The proof constructs a nested sequence of closed intervals $I_{0} \supseteq I_{1} \supseteq I_{2} \supseteq \dots$ together with an increasing sequence of indices $n_{1} < n_{2} < \dots$ such that each $I_{k}$ has length $2 M / 2^{k}$ and contains $a_{n_{k}}$ together with infinitely many other terms of the sequence.

The construction is recursive. At step $k = 0$ , set $I_{0} = [- M, M]$ and $n_{0} = 1$ ; the interval $I_{0}$ contains infinitely many terms of $(a_{n})$ since it contains all of them. Given the interval $I_{k} = [c, d]$ of length $2 M / 2^{k}$ together with infinitely many terms of $(a_{n})$ inside it, bisect $I_{k}$ into two closed subintervals of length $2 M / 2^{k + 1}$ , namely $[c, (c + d) /2]$ and $[(c + d) /2, d]$ . The union of these two subintervals is $I_{k}$ , and each contains infinitely many or finitely many terms of $(a_{n})$ . The union infinite, so at least one of the two halves contains infinitely many terms. Choose such a half and call it $I_{k + 1}$ . Since infinitely many terms of $(a_{n})$ lie in $I_{k + 1}$ , and only finitely many have index at most $n_{k}$ , an index $n_{k + 1} > n_{k}$ exists with $a_{n_{k + 1}} \in I_{k + 1}$ .

The resulting nested sequence $(I_{k})$ has interval lengths $2 M / 2^{k} \to 0$ . By the nested-interval property — a direct consequence of the completeness axiom of 02.02.01 — the intersection $⋂_{k} I_{k}$ contains a unique real number $L$ . For each $k$ , both $a_{n_{k}}$ and $L$ lie in $I_{k}$ , so $∣ a_{n_{k}} - L ∣ \leq 2 M / 2^{k}$ . Given $ε > 0$ , the Archimedean property of 02.02.01 supplies an index $K$ with $2 M / 2^{K} < ε$ ; for every $k \geq K$ this forces $∣ a_{n_{k}} - L ∣ < ε$ . Hence $a_{n_{k}} \to L$ , and $(a_{n_{k}})$ is the convergent subsequence. $□$

Theorem (Cauchy criterion). A sequence $(a_{n})$ in $R$ converges iff it is Cauchy.

Proof. $(\Rightarrow)$ Suppose $a_{n} \to L$ . Fix $ε > 0$ and choose $N$ such that $n \geq N$ implies $∣ a_{n} - L ∣ < ε /2$ . For $m, n \geq N$ , the triangle inequality gives $∣ a_{m} - a_{n} ∣ \leq ∣ a_{m} - L ∣ + ∣ L - a_{n} ∣ < ε /2 + ε /2 = ε$ . So $(a_{n})$ is Cauchy.

$(\Leftarrow)$ Suppose $(a_{n})$ is Cauchy. Three steps:

Step 1 (Cauchy implies bounded). Take $ε = 1$ in the Cauchy condition: some $N_{0}$ satisfies $∣ a_{m} - a_{n} ∣ < 1$ for $m, n \geq N_{0}$ . For $n \geq N_{0}$ , the triangle inequality gives $∣ a_{n} ∣ \leq ∣ a_{n} - a_{N_{0}} ∣ + ∣ a_{N_{0}} ∣ < 1 + ∣ a_{N_{0}} ∣$ . Set $M = max {∣ a_{1} ∣, ∣ a_{2} ∣, \dots, ∣ a_{N_{0} - 1} ∣, 1 + ∣ a_{N_{0}} ∣}$ ; then $∣ a_{n} ∣ \leq M$ for every $n$ .

Step 2 (a convergent subsequence exists). By Bolzano-Weierstrass applied to the bounded sequence $(a_{n})$ , a subsequence $(a_{n_{k}})$ converges to some $L \in R$ .

Step 3 (the full sequence converges to the same limit). Fix $ε > 0$ . By the Cauchy condition, choose $N_{1}$ so that $m, n \geq N_{1}$ implies $∣ a_{m} - a_{n} ∣ < ε /2$ . By the subsequence convergence, choose $K$ so that $k \geq K$ implies $∣ a_{n_{k}} - L ∣ < ε /2$ . Choose any $k \geq K$ with $n_{k} \geq N_{1}$ — such $k$ exists because $n_{k} \to \infty$ as $k \to \infty$ , by strict monotonicity of $k \mapsto n_{k}$ . For every $n \geq N_{1}$ , $∣ a_{n} - L ∣ \leq ∣ a_{n} - a_{n_{k}} ∣ + ∣ a_{n_{k}} - L ∣ < ε /2 + ε /2 = ε$ . So $a_{n} \to L$ . $□$

Bridge. The Cauchy criterion and Bolzano-Weierstrass are two faces of one structural fact about $R$ : completeness. The LUB axiom of 02.02.01 guarantees a least upper bound for every non-empty bounded-above subset; that axiom, paired with the Archimedean property, gives the nested-interval property; the nested-interval property powers the bisection construction in Bolzano-Weierstrass; Bolzano-Weierstrass, combined with the triangle inequality, gives the Cauchy criterion. Reversing the chain, the Cauchy criterion plus Archimedean recovers the LUB axiom — given a non-empty bounded-above $S$ with an upper bound $β$ , repeated halving of an interval to track a candidate supremum produces a Cauchy sequence whose limit is exactly $sup S$ . The four reformulations of completeness — LUB, Cauchy convergence, nested intervals, monotone convergence — are inter-derivable over the Archimedean ordered field axioms, and each reformulation is the natural one in a different context: LUB for subsets, Cauchy for sequences with unknown limit, nested intervals for bisection arguments, monotone convergence for ordered sequences. The pair developed in this unit is the metric face of completeness, the face that survives the move from $R$ to general metric spaces in 02.01.05 and beyond. Taking these together, completeness is the structural feature that makes calculus possible: limits exist when they ought to, integrals exist for continuous integrands, fixed points exist for contractive maps, and every $ε$ -argument from 02.02.01 forward draws on one of these four equivalent forms.

Exercises [Intermediate+]

Exercise 6 (hard, short-answer).

Prove that the Cauchy criterion (every Cauchy sequence converges) implies the monotone convergence theorem (every bounded-above monotone-increasing sequence converges).

Hint

Show that a bounded-above monotone-increasing sequence is Cauchy.

Answer

Let $(a_{n})$ be monotone increasing with $a_{n} \leq B$ for all $n$ . The sequence is bounded. Show it is Cauchy: suppose for contradiction that some $ε_{0} > 0$ has, for every $N$ , indices $m > n \geq N$ with $a_{m} - a_{n} \geq ε_{0}$ . Iterating, pick $n_{1} < n_{2} < n_{3} < \dots$ with $a_{n_{k + 1}} - a_{n_{k}} \geq ε_{0}$ . By monotonicity $a_{n_{k}} \geq a_{n_{1}} + (k - 1) ε_{0}$ , exceeding $B$ for $k$ large, against the bound. So $(a_{n})$ is Cauchy; by the Cauchy criterion, $a_{n} \to L$ for some $L \in R$ . Rubric: full credit for the boundedness-to-Cauchy contradiction.

Exercise 7 (hard, short-answer).

Exhibit a metric space in which the Bolzano-Weierstrass conclusion fails: a bounded sequence with no convergent subsequence. Identify which axiom of $R$ the example uses.

Hint

The standard-basis sequence in $ℓ^{2}$ is bounded but spreads out.

Answer

In the Hilbert space $ℓ^{2} = {(x_{1}, x_{2}, \dots) : \sum x_{i}^{2} < \infty}$ with the norm $∥ x ∥_{2} = (\sum x_{i}^{2})^{1/2}$ , consider the sequence $e_{n} = (0, \dots, 0, 1, 0, \dots)$ with the $1$ in the $n$ -th position. Every $∥ e_{n} ∥_{2} = 1$ , so the sequence is bounded. For $m \neq = n$ , $∥ e_{m} - e_{n} ∥_{2} = 2$ . Any subsequence has pairwise distances $2$ , so no subsequence can be Cauchy, and no subsequence converges. The example uses finite-dimensional boundedness implicitly: Bolzano-Weierstrass in $R^{n}$ uses the nested-interval property, which depends on the completeness of $R$ together with the finite dimension of the bounding box. In $ℓ^{2}$ , bounded sets are not totally bounded, so the bisection argument fails. Rubric: full credit for the $e_{n}$ construction and the dimension-or-total-boundedness explanation.

Lean formalization [Intermediate+]

lean_status: partial — Mathlib provides the Cauchy criterion, the completeness of $R$ , and the Bolzano-Weierstrass theorem in the bornology framework. The Codex module gathers these under one namespace, records the textbook form of each statement, and flags the missing single-package theorem.

[object Promise]

The full companion module at Codex.Analysis.Sequences.CauchyBolzanoWeierstrass adds the unified Cauchy-convergence equivalence and records the textbook-packaging gap.

Advanced results [Master]

The Cauchy criterion and Bolzano-Weierstrass admit generalisations along three independent axes: from $R$ to general metric spaces, from sequences to nets and filters, and from classical to constructive foundations. Each axis exposes a different aspect of completeness.

Theorem (Cauchy completeness in metric spaces). A metric space $(X, d)$ is complete iff every Cauchy sequence in $X$ converges to a point of $X$ . The space $R$ with the Euclidean metric is complete; the space $Q$ with the restricted Euclidean metric is not; every Banach space is complete by the defining axiom of 02.11.04.

Theorem (Cauchy completion). Every metric space $(X, d)$ embeds isometrically as a dense subset of a complete metric space $(\hat{X}, \hat{d})$ , unique up to isometry. The construction takes $\hat{X}$ to be the set of equivalence classes of Cauchy sequences in $X$ under the equivalence $(x_{n}) \sim (y_{n})$ iff $d (x_{n}, y_{n}) \to 0$ , with $\hat{d}$ inherited from $d$ via the diagonal. The map $X \to \hat{X}$ sends $x$ to the class of the constant sequence $(x, x, x, \dots)$ . ^{[Bourbaki Ch. II §3]}

The classical construction of $R$ from $Q$ via Cauchy sequences (Cantor 1872) ^{[Cauchy 1821]} is the prototype: $R$ is the Cauchy completion of $Q$ under the absolute-value metric. The construction is functorial — a uniformly continuous map $f : X \to Y$ extends uniquely to a uniformly continuous map $\hat{f} : \hat{X} \to \hat{Y}$ — and reproduces $R$ up to the unique order-isomorphism guaranteed by the categoricity result of 02.02.01.

Theorem (Bolzano-Weierstrass in $R^{n}$ ). Every bounded sequence in $R^{n}$ has a convergent subsequence. The proof iterates the one-dimensional argument along each coordinate axis, extracting subsubsequences and applying Bolzano-Weierstrass to each.

Theorem (sequential compactness and compactness in metric spaces). Let $(X, d)$ be a metric space. The following are equivalent:

(i) every open cover of $X$ has a finite subcover (compactness); (ii) every sequence in $X$ has a convergent subsequence (sequential compactness); (iii) $X$ is complete and totally bounded.

The equivalence (i) $\Leftrightarrow$ (ii) for metric spaces is delicate: in general topological spaces the two notions diverge. The Stone-Čech compactification $β N$ is compact but not sequentially compact (no convergent subsequence of the inclusion $N ↪ β N$ ); a sequentially compact non-compact space arises in the long-line construction. Metric spaces, and more generally first-countable Hausdorff spaces, are the natural setting where sequences suffice. ^{[Munkres §28]}

Theorem (Heine-Borel in $R^{n}$ ). A subset $K \subseteq R^{n}$ is compact iff it is closed and bounded. The forward direction uses that compact subsets of any Hausdorff space are closed and that compactness implies boundedness in any metric space. The converse uses Bolzano-Weierstrass: a closed bounded set is sequentially compact (sequences have convergent subsequences whose limits land back inside, by closedness), and sequential compactness coincides with compactness in metric spaces.

Failure of Bolzano-Weierstrass in infinite dimensions. In the Hilbert space $ℓ^{2}$ , the closed unit ball is bounded but not compact, because the standard-basis sequence $(e_{n})$ has pairwise distance $2$ and so admits no Cauchy subsequence. The failure characterises finite-dimensional normed spaces: a Banach space has compact closed unit ball iff it is finite-dimensional (Riesz's lemma plus a covering argument). The failure of Heine-Borel in $ℓ^{2}$ is the reason the spectral theory of compact operators in 02.11.04 cannot proceed by bare boundedness arguments and requires the additional ingredient of weak compactness from the Banach-Alaoglu theorem.

Banach's contraction principle. Let $(X, d)$ be a complete metric space and $T : X \to X$ a contraction with constant $q \in [0, 1)$ , meaning $d (T x, T y) \leq q d (x, y)$ for every $x, y$ . Then $T$ has a unique fixed point $x^ \in X $, an df or e v er y$ x_0 \in X $t h e i t er a t es$ T^n x_0 $co n v er g e t o$ x^$.

The proof shows that $(T^{n} x_{0})$ is Cauchy because $d (T^{n + 1} x_{0}, T^{n} x_{0}) \leq q^{n} d (T x_{0}, x_{0})$ and the geometric series $\sum q^{n}$ converges; completeness delivers the limit; uniqueness follows from the contraction estimate applied at the fixed point. The principle is the workhorse behind the Picard-Lindelöf theorem for ordinary differential equations and the inverse-function theorem on Banach spaces, and it uses Cauchy completeness as its only hypothesis on the underlying space.

Constructive content. In the Bishop-Bridges constructive analysis programme, the Cauchy criterion is the working definition of convergence: a real number is a Cauchy sequence of rationals equipped with a modulus of convergence — an explicit function $ω : N \to N$ such that $∣ a_{m} - a_{n} ∣ < 1/ k$ whenever $m, n \geq ω (k)$ . Bolzano-Weierstrass in its classical form fails constructively: the bisection argument requires a choice at each step between two halves, and the disjunction "left half has infinitely many terms or right half does" is non-effective when the sequence does not provide an effective method of decision. A weaker constructive version — every Cauchy sequence with explicit modulus has a limit — is the substitute. The classical equivalence with the LUB axiom of 02.02.01 hides this dependence on the law of the excluded middle, exposed only in the constructive reformulation.

Synthesis. The Cauchy criterion and Bolzano-Weierstrass identify completeness as the structural fact that makes real analysis cohere. The LUB axiom of 02.02.01 is the order-theoretic face; the Cauchy criterion is the metric face; Bolzano-Weierstrass is the compactness face; the nested-interval property is the geometric face. Each face emphasises a different working framework. The order-theoretic face powers supremum-and-infimum manipulations and the proofs of 02.02.02 pending sup/inf properties. The metric face survives the move to general metric spaces in 02.01.05 and is the only face that generalises to infinite-dimensional Banach and Hilbert spaces in 02.11.04. The compactness face is the lynchpin of the extreme-value theorem, the existence of integrals via Riemann sums, and the proof of Heine-Cantor uniform continuity. The geometric face is the working tool in bisection proofs and in the construction of pathological examples. Drawing the four together gives the picture in which $R$ is the unique structure where every $ε$ -argument lands inside the space; in which compactness on the line equals closed-plus-bounded; and in which the move to $ℓ^{2}$ or to the long line breaks one of the four faces at a time, revealing which axiom each piece of analysis actually uses. The Cauchy completion functor universalises the construction: every metric space embeds into its completion, and the embedding is initial among isometric embeddings into complete metric spaces — a universal property that recovers $R$ as the completion of $Q$ and Banach spaces as the completions of normed function spaces such as $C ([a, b])$ under the $L^{p}$ norms.

Full proof set [Master]

Proposition (uniqueness of limit). If $a_{n} \to L$ and $a_{n} \to L^{'}$ in $R$ , then $L = L^{'}$ .

Proof. Fix $ε > 0$ . Choose $N$ so $n \geq N$ gives both $∣ a_{n} - L ∣ < ε /2$ and $∣ a_{n} - L^{'} ∣ < ε /2$ . Triangle inequality: $∣ L - L^{'} ∣ \leq ∣ L - a_{N} ∣ + ∣ a_{N} - L^{'} ∣ < ε$ . Since $ε$ is arbitrary, $L = L^{'}$ . $□$

Proposition (Cauchy implies bounded). Every Cauchy sequence in $R$ is bounded.

Proof. As in Step 1 of the Cauchy-criterion proof: take $ε = 1$ , find $N_{0}$ with $∣ a_{n} - a_{N_{0}} ∣ < 1$ for $n \geq N_{0}$ , set $M = max {∣ a_{1} ∣, \dots, ∣ a_{N_{0} - 1} ∣, 1 + ∣ a_{N_{0}} ∣}$ . $□$

Proposition (Bolzano-Weierstrass). Proved in §"Key theorem with proof" above.

Proposition (Cauchy criterion). Proved in §"Key theorem with proof" above.

Proposition (Bolzano-Weierstrass in $R^{n}$ ). Every bounded sequence $(x^{(k)}) \subset R^{n}$ has a convergent subsequence.

Proof. The coordinate sequences $(x_{j}^{(k)})_{k \geq 1}$ for $j = 1, \dots, n$ are bounded real sequences. Apply Bolzano-Weierstrass on $R$ to the first coordinate, extracting a subsequence on which the first coordinate converges. Apply Bolzano-Weierstrass to the second coordinate along that subsequence, refining to a sub-subsequence on which both first and second coordinates converge. Iterate $n$ times. The final sub-subsequence converges in every coordinate, hence in $R^{n}$ with respect to any equivalent norm. $□$

Proposition (Heine-Borel in $R^{n}$ ). A subset $K \subseteq R^{n}$ is compact iff it is closed and bounded.

Proof. $(\Rightarrow)$ Compact subsets of any Hausdorff space are closed. For boundedness, cover $K$ by open balls $B_{r} (0)$ of growing radius $r = 1, 2, 3, \dots$ ; the cover has a finite subcover, whose union is contained in $B_{M} (0)$ for some $M$ .

$(\Leftarrow)$ Let $K \subseteq R^{n}$ be closed and bounded. Every sequence in $K$ is bounded, hence by Bolzano-Weierstrass in $R^{n}$ admits a convergent subsequence; the limit lies in $K$ by closedness. So $K$ is sequentially compact, and on a metric space sequential compactness equals compactness. $□$

Proposition (Banach contraction principle). Let $(X, d)$ be complete and $T : X \to X$ satisfy $d (T x, T y) \leq q d (x, y)$ for some $q \in [0, 1)$ . Then $T$ has a unique fixed point.

Proof. Fix $x_{0} \in X$ and set $x_{n} = T^{n} x_{0}$ . Iterating, $d (x_{n + 1}, x_{n}) \leq q^{n} d (x_{1}, x_{0})$ . For $m > n$ , the triangle inequality and the geometric series bound give

$d (x_{m}, x_{n}) \leq k = n \sum m - 1 d (x_{k + 1}, x_{k}) \leq d (x_{1}, x_{0}) k = n \sum m - 1 q^{k} \leq \frac{q ^{n}}{1 - q} d (x_{1}, x_{0}) .$

As $n \to \infty$ , $q^{n} \to 0$ , so $(x_{n})$ is Cauchy. By completeness, $x_{n} \to x^{*}$ for some $x^{*} \in X$ . The map $T$ is continuous (the contraction condition implies $∥ T x - T y ∥ \leq q ∥ x - y ∥$ , a Lipschitz bound), so $T x_{n} \to T x^{*}$ ; but $T x_{n} = x_{n + 1} \to x^{*}$ . Hence $T x^{*} = x^{*}$ .

Uniqueness: if $T x^{*} = x^{*}$ and $T y^{*} = y^{*}$ , then $d (x^{*}, y^{*}) = d (T x^{*}, T y^{*}) \leq q d (x^{*}, y^{*})$ , forcing $d (x^{*}, y^{*}) = 0$ since $q < 1$ . $□$

Proposition (Cauchy completion exists and is unique). Every metric space $(X, d)$ admits a Cauchy completion $(\hat{X}, \hat{d})$ , unique up to isometry over $X$ .

Proof sketch. Define $\hat{X}$ to be the set of equivalence classes of Cauchy sequences in $X$ under the equivalence $(x_{n}) \sim (y_{n}) ⟺ d (x_{n}, y_{n}) \to 0$ . Define $\hat{d} ([(x_{n})], [(y_{n})]) = lim_{n} d (x_{n}, y_{n})$ ; the limit exists in $R$ by the Cauchy criterion applied to the sequence $d (x_{n}, y_{n})$ , since $∣ d (x_{n}, y_{n}) - d (x_{m}, y_{m}) ∣ \leq d (x_{n}, x_{m}) + d (y_{n}, y_{m})$ . The map $X \to \hat{X}$ sends $x$ to the class of the constant sequence. Density: every Cauchy sequence in $X$ converges in $\hat{X}$ to its own equivalence class. Completeness of $\hat{X}$ : a Cauchy sequence in $\hat{X}$ is a Cauchy sequence of equivalence classes, and a diagonalisation produces a representing Cauchy sequence in $X$ whose class is the limit. Uniqueness: any complete metric space $(Y, δ)$ containing $X$ densely with the inherited metric is isometric to $\hat{X}$ over $X$ by the universal property — every isometric embedding $X \to Z$ into a complete metric space extends uniquely to an isometric embedding $\hat{X} \to Z$ . ^{[Bourbaki Ch. II §3]} $□$

Connections [Master]

The Cauchy criterion is the metric specialisation of completeness used throughout 02.01.05 (metric space). The same Cauchy-sequence-equivalence-class construction that builds $R$ from $Q$ builds the completion $\hat{X}$ of any metric space $X$ , the $L^{p}$ spaces of Lebesgue-integrable functions from the simple-function spaces, and the Banach completion of normed vector spaces in 02.11.04. Every appearance of Cauchy completeness in the curriculum traces back to the equivalence proved here.

Bolzano-Weierstrass underwrites the compactness theorems of 02.01.02 (compact spaces) and 02.04.02 pending (continuous functions on compact intervals). The Heine-Borel theorem in $R^{n}$ — closed and bounded equals compact — depends on Bolzano-Weierstrass for the bounded-implies-sequentially-compact direction, and sequential compactness equals topological compactness on metric spaces. The extreme-value theorem on a closed bounded interval, the intermediate-value theorem via interval-bisection, and the integrability of continuous functions on $[a, b]$ in 02.04.03 pending all draw on Bolzano-Weierstrass at the structural level.

The Cauchy-Banach contraction principle in 02.11.04 uses Cauchy completeness as its only hypothesis on the ambient space. The principle proves the Picard-Lindelöf existence theorem for ordinary differential equations and the inverse-function theorem on Banach spaces; both downstream applications inherit the dependence on the equivalence of Cauchy convergence with limit existence proved in this unit.

The failure of Bolzano-Weierstrass in $ℓ^{2}$ — the standard-basis sequence with pairwise distance $2$ — is the entry point to weak compactness, the Banach-Alaoglu theorem, and the spectral theory of compact operators in 02.11.04. The transition from finite-dimensional to infinite-dimensional analysis is precisely the transition from Heine-Borel to its failure, with weak topology and reflexive Banach spaces as the substitute machinery.

The construction of $R$ from $Q$ via Cauchy sequences from 02.02.01 is the historical precursor to the Cauchy completion of an arbitrary metric space. The equivalence of the construction with the LUB axiom of 02.02.01 is what licences calculus textbooks to axiomatise $R$ rather than construct it. The Cauchy-completion functor sits parallel to the LUB-supremum operator: the first organises completeness as a universal property in the category of metric spaces, the second organises completeness as a least-upper-bound statement in the order-theoretic setting.

Historical & philosophical context [Master]

Bernard Bolzano's 1817 Rein analytischer Beweis des Lehrsatzes (Prague) ^{[Bolzano 1817]} introduced the bounded-set-clustering lemma now bearing his name, in the course of giving the first analytic proof of the intermediate value theorem. Bolzano framed the result as a tool for an existence argument: a continuous function changing sign on a bounded interval must vanish somewhere inside, because the supremum of the set where the function is negative is a candidate zero whose existence the lemma supplies. The lemma sat dormant in the German-reading mathematical community for half a century, recovered only after Weierstrass's Berlin lectures in the 1860s gave the bisection proof that became standard. The bisection argument was published in Weierstrass's Werke (1894-1895) ^{[Weierstrass 1894]}.

Augustin-Louis Cauchy's Cours d'analyse of 1821 ^{[Cauchy 1821]} introduced the Cauchy criterion as a working definition of convergence — Cauchy stated that a sequence converges iff its terms eventually cluster against each other, and used the criterion freely without proving that Cauchy sequences in $R$ always have limits. Cauchy worked in the implicit setting of the "real numbers" as understood by Euler and Lagrange — a notion of magnitude rather than an axiomatised structure — so the assumption that Cauchy sequences converge was a kind of geometric postulate rather than a derivable theorem. Cantor's 1872 construction ^{[Cantor 1872]} of $R$ from $Q$ via equivalence classes of Cauchy sequences is the construction that justified Cauchy's working assumption, and Dedekind's 1872 cuts gave the order-theoretic alternative.

The modern unified treatment of the two theorems in Apostol's Calculus Vol. 1 Ch. 10 ^{[Apostol Ch. 10]} and Rudin's Principles of Mathematical Analysis Ch. 3 ^{[Rudin Ch. 3]} organises them as twin metric reformulations of the LUB axiom. Bourbaki's Topologie Générale Ch. II §3 ^{[Bourbaki Ch. II §3]} generalised both to uniform spaces, identifying completeness as a uniform-structural property and the Cauchy completion as a universal construction.

Bibliography [Master]

[object Promise]

Prerequisites

02.02.01

Tier anchors

beginner: Strogatz informal 'clustering' framing; 3Blue1Brown style sequence-convergence visualisation
intermediate: Apostol *Calculus* Vol. 1 Ch. 10 §10.7–10.13; Rudin *Principles of Mathematical Analysis* Ch. 3
master: Bolzano 1817 *Rein analytischer Beweis des Lehrsatzes* (originator of the bounded-set-clustering lemma); Weierstrass 1860s Berlin lectures (published 1885); Cauchy 1821 *Cours d'analyse* (originator of the Cauchy criterion); Apostol *Calculus* Vol. 1 Ch. 10; Bourbaki *Topologie Générale* Ch. II §3

References

TODO_REF
Apostol — Calculus Vol. 1 · Ch. 10 §10.7–10.13, Cauchy criterion, Bolzano-Weierstrass theorem, and the equivalence of Cauchy convergence with sequential convergence in $\mathbb{R}$
TODO_REF
Rudin — Principles of Mathematical Analysis · Ch. 3, sequences in metric spaces, Cauchy criterion, subsequences
TODO_REF
Bolzano 1817 — Rein analytischer Beweis des Lehrsatzes · Prague 1817, originator of the bounded-clustering lemma, presented inside the proof of the intermediate value theorem
TODO_REF
Weierstrass — Berlin lectures 1860s, *Werke* 1894–1895 · the bisection proof of the bounded-clustering theorem, standardised in his Berlin teaching
TODO_REF
Cauchy 1821 — Cours d'analyse · introduction of the Cauchy criterion as the working definition of convergence; Cauchy assumed without proof that Cauchy sequences converge
TODO_REF
Bourbaki — Topologie Générale · Ch. II §3, completeness in uniform spaces and the metric-space specialisation
TODO_REF
Munkres — Topology · §28, sequential compactness, compactness, and the gap in non-metrisable spaces

Lean module

Codex.Analysis.Sequences.CauchyBolzanoWeierstrass

Mathlib gap

Mathlib carries the Cauchy criterion through `Metric.cauchySeq_iff`, the
completeness of $\mathbb{R}$ through the `CompleteSpace ℝ` instance and
`cauchySeq_tendsto_of_complete`, and the Bolzano-Weierstrass theorem
through `tendsto_subseq_of_bounded` on the bornology of $\mathbb{R}$.
What is not packaged is a single textbook-style namespace gathering the
Apostol Ch. 10 form of the two theorems side by side: the working
$|a_m - a_n| < \varepsilon$ statement, the explicit bisection proof
of Bolzano-Weierstrass producing a strictly monotone index map, and the
unified statement that Cauchy convergence equals limit existence on
$\mathbb{R}$ in textbook calculus form. The Codex statements collect
these and record the gap as a packaging task rather than a missing
mathematical result.

Reviewer

TBD

Estimated time

beginner: 16m
intermediate: 38m
master: 60m