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

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

Contents

< real numbers

Definition

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 sequentially Cauchy complete if every Cauchy sequence in FF converges:

isCauchy(x)ϵF +.NI.iI.jI.(iN)(jN)(|x ix j|<ϵ)isCauchy(x) \coloneqq \forall \epsilon \in F_{+}. \exists N \in I. \forall i \in I. \forall j \in I. (i \geq N) \wedge (j \geq N) \wedge (\vert x_i - x_j \vert \lt \epsilon)
isLimit(x,l)ϵF +.NI.iI.(iN)(|x il|<ϵ)isLimit(x, l) \coloneqq \forall \epsilon \in F_{+}. \exists N \in I. \forall i \in I. (i \geq N) \to (\vert x_i - l \vert \lt \epsilon)
xF .isCauchy(x)lF.isLimit(x,l)\forall x \in F^\mathbb{N}. isCauchy(x) \wedge \exists l \in F. isLimit(x, l)

See also

Last revised on June 16, 2022 at 18:34:23. See the history of this page for a list of all contributions to it.