#Contents# * table of contents {:toc} ## 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 the domain tends to a term $c:S$ is a term $L:S$ 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$$ 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]]