Homotopy Type Theory computable real numbers > history (changes)

Showing changes from revision #1 to #2: Added | Removed | Changed


< computable real number

A computable real number is an element of an

Archimedean ordered field FF with either

ϵ(c): a: b:(a,b)((a,c)+(c,b))\epsilon(c):\prod_{a:\mathbb{Q}} \prod_{b:\mathbb{Q}} (a,b) \to ((a,c) + (c,b))

See also

Last revised on June 14, 2022 at 20:38:54. See the history of this page for a list of all contributions to it.