Homotopy Type Theory computable real numbers > history (changes)

Showing changes from revision #1 to #2: Added | ~~Removed~~ | ~~Chan~~ged

~~Definition~~

~~A computable real number is an element of an~~

~~Archimedean ordered field~~ ~~$F$~~ ~~with either~~

A Cauchy sequence of rational numbers $s:\mathbb{N} \to \mathbb{Q}$ with a modulus of Cauchy convergence $M:\mathbb{Q}_{+} \to \mathbb{N}$

A $Q$ -indexed locator

~~$\epsilon(c):\prod_{a:\mathbb{Q}} \prod_{b:\mathbb{Q}} (a,b) \to ((a,c) + (c,b))$~~
~~See also~~

real numbesr?

locator

Cauchy sequence

modulus of Cauchy convergence

Cauchy approximation

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