#
Homotopy Type Theory
Cauchy complete Archimedean ordered field > history (changes)

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

# Contents

< real numbers

~~
~~## Definition

~~
~~Let $F$ be an Archimedean ordered field and let

~~
~~$F_{+} \coloneqq \sum_{a:F} 0 \lt a$

~~
~~be the positive elements in $F$. $F$ is **Cauchy complete** if every Cauchy net in $F$ converges:

~~
~~$\prod_{I:\mathcal{U}} isDirected(I) \times \prod_{x:I \to F} isCauchy(x) \times \Vert \sum_{l:F} isLimit(x, l) \Vert$

~~
~~## Examples

~~
~~
- The type of real numbers $\mathbb{R}$ is a Cauchy complete Archimedean ordered field.

~~
~~## See also

~~
~~
Last revised on June 10, 2022 at 00:51:12.
See the history of this page for a list of all contributions to it.