[[!redirects Cauchy sequence]] #Contents# * table of contents {:toc} ## Definition ## ### In premetric spaces ### Let $R$ be a [[Archimedean ordered integral domain]] with a [[dense]] [[strict order]], let $R_{+}$ be the [[semiring]] of positive terms in $R$, and let $A$ be a $R_{+}$-[[premetric space]]. Given a [[directed type]] $I$, a net $a: I \to A$ is a __Cauchy net__ if $$x:I \to A \vdash c(x):\prod_{\epsilon:R_{+}} \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$$ A __Cauchy sequence__ is a Cauchy net whose index type is the [[natural numbers]] $\mathbb{N}$. ### In Cauchy spaces ### ... ## See also ## * [[Cauchy approximation]] * [[Cauchy structure]] * [[premetric space]] * [[net]] * [[filter]]