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

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

Contents

Definition
Examples
See also

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.