#Contents# * table of contents {:toc} ## Definition ## ### In rational numbers ### Let $\mathbb{Q}$ be the [[rational numbers]] and let $\mathbb{Q}_{+}$ be the positive rational numbers. The __limit of a function__ $f:\mathbb{Q} \to \mathbb{Q}$ approaching a term $c:\mathbb{Q}$ is a term $L:\mathbb{Q}$ such that for all [[directed type]]s $I$ and [[net]]s $x:I \to \mathbb{Q}$ where $c$ is the [[limit of a net|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{Q}_{+}} \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{Q}_{+}} \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 $R$ be a dense integral subdomain of the [[rational numbers]] $\mathbb{Q}$ and $R_{+}$ be the positive terms of $R$. Let $S$ and $T$ be $R_{+}$-[[premetric space]]s. The __limit of a function__ $f:S \to T$ approaching a term $c:S$ is a term $L:T$ such that for all [[directed type]]s $I$ and [[net]]s $x:I \to S$ where $c$ is the [[limit of a net|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:R_{+}} \Vert \sum_{N:I} \prod_{i:I} (i \geq N) \to (x_i \sim_\epsilon c) \Vert$$ $$isLimit(L,f \circ x) \coloneqq \prod_{\epsilon:R_{+}} \Vert \sum_{N:I} \prod_{i:I} (i \geq N) \to (f(x_i) \sim_\epsilon L) \Vert$$ The limit is usually written as $$L \coloneqq \lim_{x \to c} f(x)$$ ### Most general definition ### Let $S$ be a type with a [[predicate]] $\to_S$ between the type of all nets in $S$ $$\sum_{I:\mathcal{U}} isDirected(I) \times (I \to S)$$ and $S$ itself, and let $T$ be a type with a [[predicate]] $\to_T$ between the type of all nets in $T$ $$\sum_{I:\mathcal{U}} isDirected(I) \times (I \to T)$$ and $T$ itself. The __limit of a function__ $f:S \to T$ approaching a term $c:S$ is a term $L:T$ such that for all [[directed type]]s $I$ and [[net]]s $x:I \to S$ where $c$ is a [[limit of a net|limit]] of $x$, $L$ is a limit of $f \circ x$, or written in type theory: $$\prod_{I:\mathcal{U}} isDirected(I) \times \prod_{x:I \to S} (x \to_S c) \times (f \circ x \to_T L)$$ ## See also ## * [[net]] * [[premetric space]] * [[limit of a net]] * [[continuous function]]