#Contents# * table of contents {:toc} ## 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$ [[limit of a net|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 ## * [[Archimedean ordered field]] * [[Cauchy net]] * [[limit of a net]]