Homotopy Type Theory limit of a function > history (Rev #2, changes)

Showing changes from revision #1 to #2: Added | ~~Removed~~ | ~~Chan~~ged

Definition
- In premetric spaces
- In convergence spaces
See also

Definition

In premetric spaces

Let $T$ be a type and let $S$ be a $T$ -premetric space. The limit of a function $f:S \to S$ as approaching ~~the~~ ~~domain~~ ~~tends~~ to a term $c:S$ is a term $L:S$ such that for all directed types $I$ and nets $x:I \to S$ where $c$ is the limit of $x$ , $L$ is the limit of $f \circ x$ , or written in type theory:

\prod_{I:\mathcal{U}} isDirected(I) \times \prod_{x:I \to S} isLimit(c, x) \times isLimit(L, f \circ x)

where

isLimit(c,x) \coloneqq \prod_{\epsilon:T} \Vert \sum_{N:I} \prod_{i:I} (i \geq N) \to (x_i \sim_\epsilon c) \Vert

The limit is usually written as

L \coloneqq \lim_{x \to c} f(x)

In convergence spaces

…

Homotopy Type Theory limit of a function > history (Rev #2, changes)

Contents

Definition

In premetric spaces

In convergence spaces

See also