#Contents# * table of contents {:toc} ## Definition ## ### For 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$. A term $l:F$ is a __limit of a sequence__ $x: \mathbb{N} \to F$ or that $x$ __converges to__ $l$ if $l$ comes with a term $$\lambda: \prod_{\epsilon:F_{+}} \Vert \sum_{N:\mathbb{N}} \prod_{i:\mathbb{N}} (i \geq N) \to (\vert x_i - l \vert \lt \epsilon) \Vert$$ The type of all limits of a net is defined as $$\lim x \coloneqq \sum_{l:F} \left(\prod_{\epsilon:F_{+}} \Vert \sum_{N:\mathbb{N}} \prod_{i:\mathbb{N}} (i \geq N) \to (\vert x_i - l \vert \lt \epsilon) \Vert\right)$$ A __limit of a sequence__ $a:\mathbb{N} \to F$ is usually written as $$\lim_{x \to \infty} a(x)$$ ### For sequential convergence spaces ### Let $S$ be a [[sequential convergence space]]. A term $l:S$ is a __limit of a sequence__ $x: \mathbb{N} \to S$ or that $x$ __converges to__ $l$ if the proposition $isLimit_S(x, l)$ is [[contractible]]. The type of all limits of a net is defined as $$\lim x \coloneqq \sum_{l:S} isLimit_S(x, l)$$ ## See also ## * [[sequence]] * [[sequentially Hausdorff space]] * [[limit of a function]] * [[Cauchy sequence]] * [[sequentially Cauchy complete Archimedean ordered field]]