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

The Cauchy completion of the rational numbers, in the sense that all Cauchy nets or Cauchy filters in the rational numbers converge.

…

Let $\mathbb{Q}$ be the rational numbers and let

$\mathbb{Q}_{+} \coloneqq \{x \in \mathbb{Q} \vert 0 \lt x\}$

be the set of positive rational numbers. Let $I$ be a directed set and

$C(I, \mathbb{Q}) \coloneqq \{x \in \mathbb{Q}^I \vert \forall \epsilon \in \mathbb{Q}_{+}. \exists N \in I. \forall i \in I. \forall j \in I. (i \geq N) \wedge (j \geq N) \wedge (\vert x_i - x_j \vert \lt \epsilon)\}$

is the set of all Cauchy nets with index set $I$ and values in $\mathbb{Q}$. Let

$CauchyNetsIn(\mathbb{Q}) \coloneqq \bigcup_{I \in Ob(DirectedSet_\mathcal{U})} C(I, \mathbb{Q})$

be the (large) set of all Cauchy nets in $\mathbb{Q}$ in a universe $\mathcal{U}$, where $DirectedSet_\mathcal{U}$ is the category of all directed sets in $\mathcal{U}$.

Let the relation $\equiv_{I, J}$ in the Cartesian product $C(I, \mathbb{Q}) \times C(J, \mathbb{Q})$ for directed sets $I$ and $J$ be defined as

$a \equiv_{I, J} b \coloneqq \forall \epsilon \in \mathbb{Q}_{+}, \exists M \in I. \forall i \in I. \exists N \in J. \forall j \in J. (i \geq M) \wedge (j \geq N) \wedge (\vert a_i - b_j \vert \lt \epsilon)$

Let a *generalized Cauchy algebra* be defined as a set $A$ with a function $\iota \in {A}^{CauchyNetsIn(\mathbb{Q})}$ such that

$\forall I \in Ob(DirectedSet_\mathcal{U}). \forall J \in Ob(DirectedSet_\mathcal{U}). \forall a \in C(I, \mathbb{Q}). \forall b \in C(J, \mathbb{Q}). (a \equiv_{I, J} b) \implies (\iota(a) = \iota(b))$

A *generalized Cauchy algebra homomorphism* is a function $f:B^A$ between Cauchy algebras $A$ and $B$ such that

$\forall a \in C(\mathbb{Q}). f(\iota_A(a)) = \iota_B(a)$

The *category of generalized Cauchy algebras* is the category $GCAlg$ whose objects $Ob(GCAlg)$ are generalized Cauchy algebras and whose morphisms $Mor(GCAlg)$ are generalized Cauchy algebra homomorphisms. The set of **generalized Cauchy real numbers**, denoted $\mathbb{R}$, is defined as the initial object in the category of Cauchy algebras.

Last revised on May 24, 2023 at 13:36:47. See the history of this page for a list of all contributions to it.