#Contents# * table of contents {:toc} ## Definition ## ### In premetric spaces ### Let $R$ be a [[Archimedean ordered integral domain]] with a [[dense]] [[strict order]], let $R_{+}$ be the [[semiring]] of positive terms in $R$, and let $S$ be a $R_{+}$-[[premetric space]]. Given a [[directed type]] $I$, a __limit of a net__ $x: I \to S$ is a term $l:S$ with $$\lambda: \prod_{\epsilon:R_{+}} \Vert \sum_{N:I} \prod_{i:I} (i \geq N) \to (x_i \sim_{\epsilon} l) \Vert$$ A __limit of a sequence__ is a limit of a net that happens to be a sequence. ### In convergence spaces ### ... ## See also ## * [[premetric space]] * [[modulus of Cauchy convergence]] * [[Cauchy structure]] * [[Cauchy approximation]] * [[HoTT book real numbers]]