A Cauchy sequence is an infinite sequence which ought to converge in the sense that successive terms get arbitrarily close together, as they would if they were getting arbitrarily close to a limit. Among sequences, only Cauchy sequences will converge; in a complete space, all Cauchy sequence converge.
The precise definition varies with the context.
A sequence of real numbers is Cauchy if, for every positive number , almost all terms are within of one another. Explicitly:
In a metric space, a sequence is Cauchy under the same condition, now relative to the metric on that space. Explicitly:
The same definition immediately applies to an extended quasipseudometric space (aka a Lawvere metric space), or anything in between.
In a gauge space, a sequence is Cauchy if this condition is satisfied for each gauging distance separately. Explicitly:
where is the collection of Cauchy filters that defines the structure of the Cauchy space.
All of the above are in fact special cases of this.
A net is a generalization of a sequence; the definitions above serve to define a Cauchy net without any change, other than allowing to be a net. This is precisely the structure of a Cauchy space; instead of defining Cauchy nets in terms of Cauchy filters as above, we may equally well define a Cauchy filter to be a proper filter whose canonical net? is Cauchy.
Note that in a complete space, every Cauchy net has a limit, not just every Cauchy sequence. Rather, a space in which every Cauchy sequence converges is called sequentially complete. Note that a metric space (or even a Lawvere metric space) is in fact complete if it is sequentially complete (although this result is not valid in some weak foundations); in particular, the real line is complete.
When Bill Lawvere idenitified Lawvere metric spaces with enriched categories over the closed monoidal poset , he identified Cauchy sequences in such spaces with certain adjunctions of bimodules, enough so that a metric space would be a Cauchy-complete space if and only if every adjunction of bimodules is induced by an enriched functor. Generalising this condition from to an arbitrary closed monoidal category, we have the concept of Cauchy-complete category.