Homotopy Type Theory Cauchy net > history (Rev #11, changes)

Showing changes from revision #10 to #11: Added | ~~Removed~~ | ~~Chan~~ged

Definition
See also

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 an $R_{+}$ -premetric space . ~~Given~~ A a ~~directed~~ net ~~type~~ $x : I \to S$ x: I \to S~~, a net~~ ~~$x: I \to S$~~ is a Cauchy net if

x:I \to S \vdash c(x):\prod_{\epsilon:R_{+}} \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 $R$ be a dense integral subdomain of the rational numbers $\mathbb{Q}$ and let $R_{+}$ be the positive terms of $R$ .

A net $x: R_{+} \to S$ is a $R_{+}$ -Cauchy approximation if

x:R_{+} \to S \vdash c(x):\prod_{\delta:R_{+}} \prod_{\eta:R_{+}} x_\delta \sim_{\delta + \eta} x_\eta

Every $R_{+}$ -Cauchy approximation is a Cauchy net indexed by $R_{+}$ . This is because $R_{+}$ is a strictly ordered type, and thus a directed type and a strictly codirected type, with $N:R_{+}$ defined as $N \coloneqq \delta \otimes \eta$ for $\delta:R_{+}$ and $\eta:R_{+}$ . $\epsilon:R_{+}$ 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}$ .