**analysis** (differential/integral calculus, functional analysis, topology)

metric space, normed vector space

open ball, open subset, neighbourhood

convergence, limit of a sequence

compactness, sequential compactness

continuous metric space valued function on compact metric space is uniformly continuous

…

…

**constructive mathematics**, **realizability**, **computability**

propositions as types, proofs as programs, computational trinitarianism

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

- The Dedekind real numbers are sequentially Cauchy complete.

- Auke B. Booij, Analysis in univalent type theory (pdf)
- Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)

Last revised on May 6, 2022 at 13:55:44. See the history of this page for a list of all contributions to it.