nLab sequentially complete space

Definition

Let $S$ be a Cauchy space (such as a uniform space or a metric space). $S$ is sequentially complete or sequentially Cauchy complete if every Cauchy sequence in $S$ converges.

We can also distinguish between the usual notion of Cauchy sequences and regular Cauchy sequences, which come with a modulus of convergence. $S$ is regularly sequentially complete if every regular Cauchy sequence in $S$ converges.

Note that this is also called “Cauchy complete space” by some areas of constructive mathematics (see e.g. the HoTT Book, Booij 2020); however the term Cauchy complete space is usually used for completeness via Cauchy nets or Cauchy filters. This is because in the presence of excluded middle, every sequentially complete metric space is a complete space.

Examples

• The Dedekind real numbers are (regularly) sequentially complete.

• The HoTT book real numbers are (regularly) sequentially complete.

Related concepts

• Cauchy space

• complete space

References

See also:

• Wikipedia, Sequentially complete

Formalization in type theory:

• Univalent Foundations Project: Homotopy Type Theory – Univalent Foundations of Mathematics (2013)

• Auke B. Booij: Analysis in univalent type theory, PhD thesis, Birmingham (2020) [pdf, pdf]