11.3.4 Cauchy reals are Cauchy complete

We constructed ℝ𝖼 by closing β„š under limits of Cauchy approximations, so it better be the case that ℝ𝖼 is Cauchy completePlanetmathPlanetmathPlanetmathPlanetmathPlanetmath. Thanks to \autorefRC-sim-eqv-le there is no differencePlanetmathPlanetmath between a Cauchy approximation x:β„š+→ℝ𝖼 as defined in the construction of ℝ𝖼, and a Cauchy approximation in the sense of \autorefdefn:cauchy-approximation (adapted to ℝ𝖼).

Thus, given a Cauchy approximation x:β„š+→ℝ𝖼 it is quite natural to expect that 𝗅𝗂𝗆⁒(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 Rc has a limit.

An archimedeanPlanetmathPlanetmathPlanetmath 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.


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 embeddingMathworldPlanetmathPlanetmath e:ℝ𝖼→F by (ℝ𝖼,∼)-recursion as

e(𝗋𝖺𝗍(q)):≑q  and  e(𝗅𝗂𝗆(x)):≑lim(e∘x).

A suitable ⌒ on F is


This is a separated relationMathworldPlanetmathPlanetmath because F is archimedean. The rest of the clauses for (ℝ𝖼,∼)-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