**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

A notion of Cauchy space where only certain Cauchy nets with a particular modulus of convergence converges in the space.

Let $S$ be a Cauchy space (such as a uniform space or a metric space). Given a directed set $I$, $S$ is **$I$-modulated Cauchy complete** if every Cauchy net in $S$ with index set $I$ and with a $I$-modulus of convergence converges.

A Cauchy space is said to be **sequentially modulated Cauchy complete** if every Cauchy sequence in $S$ with a $\mathbb{N}$-modulus of convergence converges.

- The Dedekind real numbers are sequentially modulated Cauchy complete.
- The HoTT book real numbers are sequentially modulated Cauchy complete.

Created on May 6, 2022 at 17:28:13. See the history of this page for a list of all contributions to it.