[[!redirects Cauchy sequence]] #Contents# * table of contents {:toc} ## Definition ## ### In premetric spaces ### Let $T$ be a [[directed type]], and let $S$ be a $T$-[[premetric space]]. Given a [[directed type]] $I$, a net $x: I \to S$ is a __Cauchy net__ if $$x:I \to S \vdash c(x):\prod_{\epsilon:T} \Vert \sum_{N:I} \prod_{i:I} \prod_{j:I} (i \geq N) \times (j \geq N) \times (x_i \sim_{\epsilon} x_j) \Vert$$ ### Cauchy approximations ### Let $A$ be a [[dense]] [[Archimedean ordered abelian group]] with a point $1:A$ and a term $\zeta: 0 \lt 1$. Let $A_{+} \coloneqq \sum_{a:A} (0 \lt a)$ be the [[positive cone]] of $A$. A net $x: A_{+} \to S$ is a __$A_{+}$-Cauchy approximation__ if $$x:R_{+} \to S \vdash c(x):\prod_{\delta:R_{+}} \prod_{\eta:R_{+}} x_\delta \sim_{\delta + \eta} x_\eta$$ Every $A_{+}$-Cauchy approximation is a [[Cauchy net]] indexed by $A_{+}$. This is because $A_{+}$ is a strictly ordered type, and thus a directed type and a strictly codirected type, with $N:A_{+}$ defined as $N \coloneqq \delta \otimes \eta$ for $\delta:A_{+}$ and $\eta:A_{+}$. $\epsilon:R_{+}$ is defined as $\epsilon + \delta + \eta$. ### In Cauchy spaces ### ... ### Cauchy sequences ### A __Cauchy sequence__ is a Cauchy net whose index type is the [[natural numbers]] $\mathbb{N}$. ## See also ## * [[Cauchy approximation]] * [[Cauchy structure]] * [[premetric space]] * [[net]] * [[filter]]