# 11.3.4 Cauchy reals are Cauchy complete

We constructed ${\mathrm{\beta \x84\x9d}}_{\mathrm{\pi \x9d\x96\u038c}}$ by closing $\mathrm{\beta \x84\x9a}$ under limits of Cauchy approximations, so it better
be the case that ${\mathrm{\beta \x84\x9d}}_{\mathrm{\pi \x9d\x96\u038c}}$ is Cauchy complete^{}. Thanks to \autorefRC-sim-eqv-le there is no
difference^{} between a Cauchy approximation $x:{\mathrm{\beta \x84\x9a}}_{+}\beta \x86\x92{\mathrm{\beta \x84\x9d}}_{\mathrm{\pi \x9d\x96\u038c}}$ as defined in the construction
of ${\mathrm{\beta \x84\x9d}}_{\mathrm{\pi \x9d\x96\u038c}}$, and a Cauchy approximation in the sense of \autorefdefn:cauchy-approximation
(adapted to ${\mathrm{\beta \x84\x9d}}_{\mathrm{\pi \x9d\x96\u038c}}$).

Thus, given a Cauchy approximation $x:{\mathrm{\beta \x84\x9a}}_{+}\beta \x86\x92{\mathrm{\beta \x84\x9d}}_{\mathrm{\pi \x9d\x96\u038c}}$ it is quite natural to expect that $\mathrm{\pi \x9d\x97\x85\pi \x9d\x97\x82\pi \x9d\x97\x86}\beta \x81\u2019(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 ${\mathrm{R}}_{\mathrm{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:{\mathrm{\beta \x84\x9d}}_{\mathrm{\pi \x9d\x96\u038c}}\beta \x86\x92F$ by $({\mathrm{\beta \x84\x9d}}_{\mathrm{\pi \x9d\x96\u038c}},\mathrm{\beta \x88\u038c})$-recursion as

$$e(\mathrm{\pi \x9d\x97\x8b\pi \x9d\x96\u038a\pi \x9d\x97\x8d}(q)):\beta \x89\u2018q\mathit{\beta \x80\x83\beta \x80\x83}\text{and}\mathit{\beta \x80\x83\beta \x80\x83}e(\mathrm{\pi \x9d\x97\x85\pi \x9d\x97\x82\pi \x9d\x97\x86}(x)):\beta \x89\u2018lim(e\beta \x88\x98x).$$ |

A suitable $\beta \x8c\u2019$ on $F$ is

$$ |

This is a separated relation^{} because $F$ is archimedean. The rest of the clauses for
$({\mathrm{\beta \x84\x9d}}_{\mathrm{\pi \x9d\x96\u038c}},\mathrm{\beta \x88\u038c})$-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 |