Homotopy Type Theory computable real numbers > history (Rev #1)


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

Revision on May 10, 2022 at 02:44:16 by Anonymous?. See the history of this page for a list of all contributions to it.