#Contents# * table of contents {:toc} ## Definition ## ### In premetric spaces ### Let $R$ be a dense integral subdomain of the [[rational numbers]] $\mathbb{Q}$ and let $R_{+}$ be the positive terms of $R$. Let $S$ be a $R_{+}$-[[premetric 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 $l$ comes with a term $$\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__ $a:\mathbb{N} \to S$ is usually written as $$\lim_{x \to \infty} a(x)$$ ### Cauchy approximations ### Let $R$ be a dense integral subdomain of the [[rational numbers]] $\mathbb{Q}$ and let $R_{+}$ be the positive terms of $R$. A limit of a $R_{+}$-[[Cauchy approximation]] $x: R_{+} \to S$ is a term $l:S$ with $$x:R_{+} \to S \vdash c(x):\prod_{\delta:R_{+}} \prod_{\eta:R_{+}} x_\delta \sim_{\delta \oplus \eta} l$$ ### In convergence spaces ### ... ## See also ## * [[net]] * [[premetric space]] * [[limit of a function]] * [[modulus of Cauchy convergence]] * [[Cauchy structure]] * [[Cauchy approximation]] * [[HoTT book real numbers]]