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

Showing changes from revision #1 to #2: Added | Removed | Changed


< real numbers


Let FF be an Archimedean ordered field and let

F + a:F0<aF_{+} \coloneqq \sum_{a:F} 0 \lt a

be the positive elements in FF. FF is Cauchy complete if every Cauchy net in FF converges:

I:𝒰isDirected(I)× x:IFisCauchy(x)× l:FisLimit(x,l)\prod_{I:\mathcal{U}} isDirected(I) \times \prod_{x:I \to F} isCauchy(x) \times \Vert \sum_{l:F} isLimit(x, l) \Vert


  • 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.