Homotopy Type Theory Cauchy sequence > history (Rev #4, changes)

Showing changes from revision #3 to #4: Added | ~~Removed~~ | ~~Chan~~ged

Contents

Definition
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$ . A sequence $x:\mathbb{N} \to F$ is a Cauchy sequence if :

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) \coloneqq \forall \epsilon \in F_{+}. \exists N \in I. \forall i \in I. (i \geq N) \to (\vert x_i - l \vert \lt \epsilon)

See also

Archimedean ordered integral domain

~~sequentially Cauchy complete Archimedean ordered integral domain?~~

Archimedean ordered field

~~sequentially Cauchy complete Archimedean ordered field~~

category: not redirected to nlab yet

Revision on June 16, 2022 at 18:35:50 by Anonymous?. See the history of this page for a list of all contributions to it.