#Contents# * table of contents {:toc} Whenever editing is allowed on the [[nLab:HomePage|nLab]] again, this article should be ported over there. ## Definition ## ### In Archimedean ordered fields ### Let $F$ be an [[Archimedean ordered field]]. The __limit of a function__ $f:\F \to F$ approaching a term $c:F$ is a term $L:F$ such that for all [[directed type]]s $I$ and [[net]]s $x:I \to F$ 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 F} isLimit(c, x) \times isLimit(L, f \circ x)$$ where $$isLimit(c,x) \coloneqq \prod_{\epsilon:(0, \infty)} \left[\sum_{N:I} \prod_{i:I} (i \geq N) \to \left[\sum_{a:(-\epsilon, \epsilon)} x_i - c = a\right]\right]$$ $$isLimit(L,f \circ x) \coloneqq \prod_{\epsilon:(0, \infty)} \left[\sum_{N:I} \prod_{i:I} (i \geq N) \to \left[\sum_{a:(-\epsilon, \epsilon)} f(x_i) - L = a\right] \right]$$ The limit is usually written as $$L \coloneqq \lim_{x \to c} f(x)$$ ### In preconvergence spaces ### Let $S$ and $T$ be [[preconvergence 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 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} isLimit_S(x, c) \times isLimit_T(f \circ x, L)$$ ### In function limit spaces ### Let $T$ be a [[function limit space]] and let $S \subseteq T$ be a [[subtype]] of $T$. The __limit of a function__ $f:S \to T$ approaching $c:S$ is a term $L:T$ such that the limit of $f$ approaching $c:S$ is equal to $L$: $$hasLimitApproaching(f, c) \coloneqq \Vert \sum_{L:T} \lim_{x \to c} f(x) = L\Vert$$ We define the type of functions with limits approaching $c$ as the dependent type $$FuncWithLim(S, T)(c) \coloneqq \sum_{f:S \to T} hasLimitApproaching(f, c)$$ ## See also ## * [[net]] * [[Archimedean ordered field]] * [[limit of a net]] * [[pointwise continuous function]]