#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 $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 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:T} \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:V} \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)$$ ### In convergence spaces ### ... ## See also ## * [[net]] * [[premetric space]] * [[limit of a net]] * [[continuous function]]