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



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

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.