#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 ### #### For 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$. Given a [[directed type]] $I$, an element $l \in F$ is a __limit of a net__ $x \in F^I$ or that $x$ __converges to__ $l$ if $$\forall \epsilon \in F_{+}. \exists N \in I. \forall i \in I. (i \geq N) \to (\vert x_i - l \vert \lt \epsilon)$$ The set of all limits of a net is defined as $$\lim x \coloneqq \{ l \in F \vert \forall \epsilon \in F_{+}. \exists N \in I. \forall i \in I. (i \geq N) \to (\vert x_i - l \vert \lt \epsilon) \}$$ A __limit of a sequence__ $a \in F^\mathbb{N}$ is usually written as $$\lim_{x \to \infty} a(x)$$ #### For preconvergence spaces #### Let $S$ be a [[preconvergence space]]. Given a [[directed type]] $I$, an element $l \in S$ is a __limit of a net__ $x \in S^I$ or that $x$ __converges to__ $l$ if $isLimit_S(x, l)$. The set of all limits of a net is defined as $$\lim x \coloneqq \{l\in S \vert isLimit_S(x, l) \}$$ ### In homotopy type theory ### #### 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$. Given a [[directed type]] $I$, a term $l:F$ is a __limit of a net__ $x: I \to F$ or that $x$ __converges to__ $l$ if $l$ comes with a term $$\lambda: \prod_{\epsilon:F_{+}} \Vert \sum_{N:I} \prod_{i:I} (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:I} \prod_{i:I} (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 preconvergence spaces #### Let $S$ be a [[preconvergence space]]. Given a [[directed type]] $I$, a term $l:S$ is a __limit of a net__ $x: I \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 ## * [[net]] * [[premetric space]] * [[Hausdorff space]] * [[limit of a function]] * [[modulus of Cauchy convergence]] * [[Cauchy structure]] * [[Cauchy approximation]] * [[HoTT book real numbers]]