Homotopy Type Theory limit of a net > history (Rev #1)

Contents

Definition
- In premetric spaces
- In convergence spaces
See also

Definition

In premetric spaces

Let $R$ be a Archimedean ordered integral domain with a dense strict order, let $R_{+}$ be the semiring? of positive terms in $R$ , and let $S$ be a $R_{+}$ -premetric space. Given a directed type $I$ , a limit of a net $x: I \to S$ is a term $l:S$ with

\lambda: \prod_{\epsilon:R_{+}} \Vert \sum_{N:I} \prod_{i:I} (i \geq N) \to (x_i \sim_{\epsilon} l) \Vert

A limit of a sequence is a limit of a net that happens to be a sequence.

In convergence spaces

…

See also

Revision on March 12, 2022 at 00:32:44 by Anonymous?. See the history of this page for a list of all contributions to it.