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

Definition

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

r:[0,1] Rr=lim n i=0 n(r) i10 i\prod_{r:[0, 1]_R} r = \lim_{n \to \infty} \sum_{i=0}^{n} \frac{\mathcal{I}(r)_i}{10^i}

Properties

  • The infinite decimal representation of the unit interval in the rational numbers consist of all the eventually periodic sequences in the natural numbers that are bounded below by 00 and bounded above by 99. Every rational number in the unit interval could be represented by two natural numbers m:m:\mathbb{N} and n:n:\mathbb{N} such that p:mnp:m \leq n. Let us define the sequences δ:\delta:\mathbb{N} \to \mathbb{N} and ρ:\rho:\mathbb{N} \to \mathbb{N} inductively as

    δ 0m÷n\delta_0 \coloneqq m \div n
    ρ 0m%n\rho_0 \coloneqq m\ \%\ n
    δ s(i)(ρ i10)÷n\delta_{s(i)} \coloneqq (\rho_i \cdot 10) \div n
    ρ s(i)(ρ i10)%n\rho_{s(i)} \coloneqq (\rho_i \cdot 10)\ \%\ n

    The sequence δ\delta is the infinite decimal representation of the rational number m/nm/n.

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

See also

Revision on May 2, 2022 at 21:48:46 by Anonymous?. See the history of this page for a list of all contributions to it.