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

# Contents

## 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

Revision on April 14, 2022 at 20:35:06 by
Anonymous?.
See the history of this page for a list of all contributions to it.