Homotopy Type Theory Cauchy net > history (Rev #2)

Contents

Definition
- In premetric spaces
- In Cauchy spaces
See also

Definition

In premetric spaces

Let $R$ be a Archimedean ordered integral domain with a dense linear order?, let $R_{+}$ be the semiring? of positive terms in $R$ , and let $A$ be a $R_{+}$ -premetric space. Given a directed type $I$ , a net $a: I \to A$ is a Cauchy net if

x:I \to A \vdash c(x):\prod_{\epsilon:R_{+}} \Vert \sum_{N:I} \prod_{i:I} \prod_{j:I} (i \geq N) \times (j \geq N) \times (x_i \sim_{\epsilon} x_j) \Vert

A Cauchy sequence is a Cauchy net whose index type is $\mathbb{N}$ .

In Cauchy spaces

…

See also

Revision on March 11, 2022 at 18:29:26 by Anonymous?. See the history of this page for a list of all contributions to it.