# 11.3.4 Cauchy reals are Cauchy complete

We constructed $\mathbb{R}_{\mathsf{c}}$ by closing $\mathbb{Q}$ under limits of Cauchy approximations, so it better be the case that $\mathbb{R}_{\mathsf{c}}$ is Cauchy complete. Thanks to \autorefRC-sim-eqv-le there is no difference between a Cauchy approximation $x:\mathbb{Q}_{+}\to\mathbb{R}_{\mathsf{c}}$ as defined in the construction of $\mathbb{R}_{\mathsf{c}}$, and a Cauchy approximation in the sense of \autorefdefn:cauchy-approximation (adapted to $\mathbb{R}_{\mathsf{c}}$).

Thus, given a Cauchy approximation $x:\mathbb{Q}_{+}\to\mathbb{R}_{\mathsf{c}}$ it is quite natural to expect that $\mathsf{lim}(x)$ is its limit, where the notion of limit is defined as in \autorefdefn:cauchy-approximation. But this is so by \autorefRC-sim-eqv-le and \autorefthm:RC-sim-lim-term. We have proved:

###### Theorem 11.3.1.

Every Cauchy approximation in $\mathbb{R}_{\mathsf{c}}$ has a limit.

An archimedean ordered field in which every Cauchy approximation has a limit is called Cauchy complete. The Cauchy reals are the least such field.

###### Theorem 11.3.2.

The Cauchy reals embed into every Cauchy complete archimedean ordered field.

###### Proof.

Suppose $F$ is a Cauchy complete archimedean ordered field. Because limits are unique, there is an operator $\lim$ which takes Cauchy approximations in $F$ to their limits. We define the embedding $e:\mathbb{R}_{\mathsf{c}}\to F$ by $(\mathbb{R}_{\mathsf{c}},{\mathord{\sim}})$-recursion as

 $e(\mathsf{rat}(q)):\!\!\equiv q\qquad\text{and}\qquad e(\mathsf{lim}(x)):\!\!% \equiv\lim(e\circ x).$

A suitable $\frown$ on $F$ is

 $(a\frown_{\epsilon}b):\!\!\equiv|a-b|<\epsilon.$

This is a separated relation because $F$ is archimedean. The rest of the clauses for $(\mathbb{R}_{\mathsf{c}},{\mathord{\sim}})$-recursion are easily checked. One would also have to check that $e$ is an embedding of ordered fields which fixes the rationals. ∎

 Title 11.3.4 Cauchy reals are Cauchy complete \metatable