## Cauchy sequences in (pseudo-)metric spaces #

Various results on Cauchy sequences in (pseudo-)metric spaces, including

`Metric.complete_of_cauchySeq_tendsto`

A pseudo-metric space is complete iff each Cauchy sequences converges to some limit point.`cauchySeq_bdd`

: a Cauchy sequence on the natural numbers is bounded- various characterisation of Cauchy and uniformly Cauchy sequences

## Tags #

metric, pseudo_metric, Cauchy sequence

A very useful criterion to show that a space is complete is to show that all sequences
which satisfy a bound of the form `dist (u n) (u m) < B N`

for all `n m ≥ N`

are
converging. This is often applied for `B N = 2^{-N}`

, i.e., with a very fast convergence to
`0`

, which makes it possible to use arguments of converging series, while this is impossible
to do in general for arbitrary Cauchy sequences.

A pseudo-metric space is complete iff every Cauchy sequence converges.

In a pseudometric space, Cauchy sequences are characterized by the fact that, eventually, the distance between its elements is arbitrarily small

A variation around the pseudometric characterization of Cauchy sequences

In a pseudometric space, uniform Cauchy sequences are characterized by the fact that, eventually, the distance between all its elements is uniformly, arbitrarily small.

If the distance between `s n`

and `s m`

, `n ≤ m`

is bounded above by `b n`

and `b`

converges to zero, then `s`

is a Cauchy sequence.

If the distance between `s n`

and `s m`

, `n, m ≥ N`

is bounded above by `b N`

and `b`

converges to zero, then `s`

is a Cauchy sequence.

A Cauchy sequence on the natural numbers is bounded.

Yet another metric characterization of Cauchy sequences on integers. This one is often the most efficient.