Homotopy Type Theory infinite decimal representation of a unit interval > history (Rev #2)

Definition

Let $R$ be an Archimedean ordered integral domain and let $[0, 1]_R$ be the unit interval in $R$. The infinite decimal representation of $[0, 1]_R$ is a function $\mathcal{I}:[0, 1]_R \to (\mathbb{N} \to [0, 9]_\mathbb{N})$ from the unit interval in $R$ to the type of sequences in the natural numbers that are bounded below by $0$ and bounded above by $9$, such that $r$ is equal to the limit of the following sequence

Properties

• The infinite decimal representation of the rational numbers consist of all the eventually periodic sequences in the natural numbers that are bounded below by $0$ and bounded above by $9$.

• The infinite decimal representation of the decimal numbers consist of all the sequences such that there is a natural number $N$ such that for all decimal number $i$ and natural numbers $n \geq N$, $\mathcal{I}(i)(n) = 0$ or $\mathcal{I}(i)(n) = 9$.

See also

• real numbers

• pre-algebra real numbers

• sequence

• limit of a sequence

• unit interval