Homotopy Type Theory pre-algebra real numbers > history (Rev #4, changes)

Showing changes from revision #3 to #4: Added | Removed | Changed

Idea

< pre-algebra real numbers

The real numbers as encountered in pre-algebra.

Definition

The pre-algebra real numbers \mathbb{R} is an Archimedean ordered field such that the infinite decimal representation function of the unit interval :[0,1] ([0,9] )\mathcal{I}:[0, 1]_\mathbb{R} \to (\mathbb{N} \to [0, 9]_\mathbb{N}) is an equivalence.

See also

Revision on June 10, 2022 at 00:11:43 by Anonymous?. See the history of this page for a list of all contributions to it.