Construction of the reals from Cauchy sequences

Summary

This construction defines the real numbers as limits of sequences of rational numbers. A sequence $(x_n)$ of rational numbers is a Cauchy sequence when, for each rational $\varepsilon > 0$, there is $N$ with $|x_m - x_n| < \varepsilon$ for all $m, n \ge N$. Two Cauchy sequences $(x_n)$ and $(y_n)$ are equivalent when $x_n - y_n$ tends to $0$: for each rational $\varepsilon > 0$, there is $N$ with $|x_n - y_n| < \varepsilon$ for all $n \ge N$. A real number is an equivalence class of Cauchy sequences of rational numbers. Addition and multiplication act term by term: $[(x_n)] + [(y_n)] = [(x_n + y_n)]$ and $[(x_n)] \cdot [(y_n)] = [(x_n y_n)]$.