11.2.2 Dedekind reals are Cauchy complete
Recall that is a Cauchy sequence when it satisfies
Note that we did not truncate the inner existential because we actually want to compute rates of convergence—an approximation without an error estimate carries little useful information. By \autorefthm:ttac, (11.2.1) yields a function , called the modulus of convergence, such that implies . From this we get for all . In fact, the map carries the same information about the limit as the original Cauchy condition (11.2.1). We shall work with these approximation functions rather than with Cauchy sequences.
A Cauchy approximation is a map which satisfies
The limit of a Cauchy approximation is a number such that
Every Cauchy approximation in has a limit.
Note that we are showing existence, not mere existence, of the limit. Given a Cauchy approximation , define
It is clear that and are inhabited, rounded, and disjoint. To establish locatedness, consider any such that . There is such that . Since merely or . In the first case we have and in the second .
To show that is the limit of , consider any . Because is dense in there merely exist such that
and thus . Now either or . In the first case we have
and in the second
In either case it follows that . ∎
For sake of completeness we record the classic formulation as well.
Suppose satisfies the Cauchy condition (11.2.1). Then there exists such that
By \autorefthm:ttac there is such that is a Cauchy approximation. Let be its limit, which exists by \autorefRD-cauchy-complete. Given any , let and observe that, for any ,
|Title||11.2.2 Dedekind reals are Cauchy complete|