\( \newcommand{\cat}[1] {\mathrm{#1}} \newcommand{\catobj}[1] {\operatorname{Obj}(\mathrm{#1})} \newcommand{\cathom}[1] {\operatorname{Hom}_{\cat{#1}}} \newcommand{\multiBetaReduction}[0] {\twoheadrightarrow_{\beta}} \newcommand{\betaReduction}[0] {\rightarrow_{\beta}} \newcommand{\betaEq}[0] {=_{\beta}} \newcommand{\string}[1] {\texttt{"}\mathtt{#1}\texttt{"}} \newcommand{\symbolq}[1] {\texttt{`}\mathtt{#1}\texttt{'}} \)

Real numbers, the construction from Cauchy Sequences

A real number is defined to be a new type of object, written as \( LIM_{n \rightarrow \infty} a_n \). This object has a (1 to many) correspondence to a Cauchy sequence \( (a_n)_{n=1}^{\infty} \). The Cauchy sequence is used to define an equivalence relation between real numbers: two real numbers \( LIM_{n \rightarrow \infty} a_n \) and \( LIM_{n \rightarrow \infty} b_n \) are said to be equal iff the corresponding sequences \( (a_n)_{n=1}^{\infty} \) and \( (b_n)_{n=1}^{\infty} \) are [...].