Homotopy Type Theory limit of a function > history (Rev #4)

Definition
See also

Definition

In real numbers

Let $\mathbb{R}$ be a type of real numbers and let $\mathbb{R}_{+}$ be the positive real numbers. The limit of a function $f:\mathbb{R} \to \mathbb{R}$ approaching a term $c:\mathbb{R}$ is a term $L:\mathbb{R}$ such that for all directed types $I$ and nets $x:I \to \mathbb{R}$ 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 \mathbb{R}} isLimit(c, x) \times isLimit(L, f \circ x)

where

isLimit(c,x) \coloneqq \prod_{\epsilon:\mathbb{R}_{+}} \Vert \sum_{N:I} \prod_{i:I} (i \geq N) \to (\vert x_i - c \vert \lt \epsilon) \Vert

isLimit(L,f \circ x) \coloneqq \prod_{\epsilon:\mathbb{R}_{+}} \Vert \sum_{N:I} \prod_{i:I} (i \geq N) \to (\vert f(x_i) - L \vert \lt \epsilon) \Vert

The limit is usually written as

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

In premetric spaces

Let $T$ be a type and let $S$ be a $T$ -premetric space and $U$ be a $V$ -premetric space. The limit of a function $f:S \to U$ approaching a term $c:S$ is a term $L:U$ 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)