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

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

See also

• real numbers

• pre-algebra real numbers

• sequence

• limit of a sequence

• unit interval