#Contents# * table of contents {:toc} Whenever editing is allowed on the [[nLab:HomePage|nLab]] again, this article should be ported over there. ## Definition ## ### In set theory ### #### In Archimedean ordered fields #### Let $F$ be an [[Archimedean ordered field]] and let $$F_{+} \coloneqq \{a \in F \vert 0 \lt a$$ be the positive elements in $F$. The __limit of a function__ $f \in F^F$ approaching an element $c \in F$ is an element $L \in F$ such that for all directed sets $I$ and [[net]]s $x \in F^I$ where $c$ is the [[limit of a net|limit]] of $x$, $L$ is the limit of $f \circ x$, or written in type theory: $$\forall I \in DirectedSet_\mathcal{U}. \forall x \in F^I isLimit(c, x) \wedge isLimit(L, f \circ x)$$ where the predicates $$isLimit(c,x) \coloneqq \forall \epsilon \in F_{+}. \exists N \in I. \forall i\in I. (i \geq N) \implies (\vert x_i - c \vert \lt \epsilon)$$ $$isLimit(L,f \circ x) \coloneqq \forall \epsilon \in F_{+}. \exists N \in I. \forall i\in I. (i \geq N) \to (\vert f(x_i) - L \vert \lt \epsilon)$$ 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 \in T^S$ approaching an element $c \in S$ is an element $L \in T$ such that for all directed sets $I$ and [[net]]s $x \in S^I$ where $c$ is a [[limit of a net|limit]] of $x$, $L$ is a limit of $f \circ x$, or written in type theory: $$\forall I \in DirectedSet_\mathcal{U}. \forall x \in S^I. isLimit_S(x, c) \times isLimit_T(f \circ x, L)$$ ### In homotopy type theory ### #### In Archimedean ordered fields #### Let $F$ be an [[Archimedean ordered field]] and let $$F_{+} \coloneqq \sum{a:F} 0 \lt a$$ be the positive elements in $F$. 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:F_{+}} \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:F_{+}} \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 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]]