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 complete. Thanks to \autorefRC-sim-eqv-le there is no difference between a Cauchy approximation as defined in the construction of , and a Cauchy approximation in the sense of \autorefdefn:cauchy-approximation (adapted to ).
Thus, given a Cauchy approximation it is quite natural to expect that 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:
Every Cauchy approximation in has a limit.
The Cauchy reals embed into every Cauchy complete archimedean ordered field.
A suitable on is
This is a separated relation because is archimedean. The rest of the clauses for -recursion are easily checked. One would also have to check that is an embedding of ordered fields which fixes the rationals. ∎
|Title||11.3.4 Cauchy reals are Cauchy complete|