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

Contents

Definition
See also

Definition

In premetric spaces

Let $T$ be a directed type, and let $S$ be a $T$ -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:T} \Vert \sum_{N:I} \prod_{i:I} (i \geq N) \to (x_i \sim_{\epsilon} l) \Vert

Of Cauchy approximations

Let $R$ be a Archimedean ordered integral domain with a dense strict order, and let $R_{+}$ be the semiring? of positive terms in $R$ . If both $T$ and $I$ are $R_{+}$ , then a limit of a Cauchy approximation $x: R_{+} \to S$ is a term $l:S$ with

x:R_{+} \to S \vdash c(x):\prod_{\delta:R_{+}} \prod_{\eta:R_{+}} x_\delta \sim_{\delta + \eta} l

In convergence spaces

…

Sequences

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

See also

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