[[!redirects Cauchy sequence]] #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 premetric spaces #### Let $\mathbb{Q}$ be the [[rational numbers]] and let $$\mathbb{Q}_{+} \coloneqq \{x \in \mathbb{Q} \vert 0 \lt x\}$$ be the positive rational numbers. Let $S$ be an [[premetric space]]. A [[net]] $x \in S^I$ is a __Cauchy net__ if $$\forall \epsilon \in \mathbb{Q}_{+}. \exists N \in I. \forall i \in I. \forall j \in I. (i \geq N) \wedge (j \geq N) \wedge (x_i \sim_{\epsilon} x_j)$$ #### Cauchy approximations #### Let $\mathbb{Q}$ be the [[rational numbers]] and let $$\mathbb{Q}_{+} \coloneqq \{x \in \mathbb{Q} \vert 0 \lt x\}$$ be the positive rational numbers. A net $x \in S^{\mathbb{Q}_{+}}$ is a __Cauchy approximation__ if $$\forall \delta \in \mathbb{Q}_{+}. \forall \eta \in \mathbb{Q}_{+}. x_\delta \sim_{\delta + \eta} x_\eta$$ Every [[Cauchy approximation]] is a Cauchy net indexed by $\mathbb{Q}_{+}$. This is because $\mathbb{Q}_{+}$ is a strictly ordered type, and thus a directed type and a strictly codirected type, with $N \in \mathbb{Q}_{+}$ defined as $N \coloneqq \delta \otimes \eta$ for $\delta \in \mathbb{Q}_{+}$ and $\eta \in \mathbb{Q}_{+}$. $\epsilon \in \mathbb{Q}_{+}$ is defined as $\epsilon \coloneqq \delta + \eta$. #### In Cauchy spaces #### ... ### In homotopy type theory ### #### In premetric spaces #### Let $\mathbb{Q}$ be the [[rational numbers]] and let $$\mathbb{Q}_{+} \coloneqq \sum_{x:\mathbb{Q}} 0 \lt x$$ be the positive rational numbers. Let $S$ be an [[premetric space]]. A [[net]] $x: I \to S$ is a __Cauchy net__ if $$x:I \to S \vdash c(x):\prod_{\epsilon:\mathbb{Q}_{+}} \Vert \sum_{N:I} \prod_{i:I} \prod_{j:I} (i \geq N) \times (j \geq N) \times (x_i \sim_{\epsilon} x_j) \Vert$$ #### Cauchy approximations #### Let $\mathbb{Q}$ be the [[rational numbers]] and let $$\mathbb{Q}_{+} \coloneqq \sum_{x:\mathbb{Q}} 0 \lt x$$ be the positive rational numbers. A net $x: \mathbb{Q}_{+} \to S$ is a __Cauchy approximation__ if $$x:\mathbb{Q}_{+} \to S \vdash c(x):\prod_{\delta:\mathbb{Q}_{+}} \prod_{\eta:\mathbb{Q}_{+}} x_\delta \sim_{\delta + \eta} x_\eta$$ Every [[Cauchy approximation]] is a Cauchy net indexed by $\mathbb{Q}_{+}$. This is because $\mathbb{Q}_{+}$ is a strictly ordered type, and thus a directed type and a strictly codirected type, with $N:\mathbb{Q}_{+}$ defined as $N \coloneqq \delta \otimes \eta$ for $\delta:\mathbb{Q}_{+}$ and $\eta:\mathbb{Q}_{+}$. $\epsilon:\mathbb{Q}_{+}$ is defined as $\epsilon \coloneqq \delta + \eta$. #### In Cauchy spaces #### ... ### Cauchy sequences ### A __Cauchy sequence__ is a Cauchy net whose index type is the [[natural numbers]] $\mathbb{N}$. ## See also ## * [[Cauchy approximation]] * [[Cauchy structure]] * [[premetric space]] * [[net]] * [[filter]]