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

Showing changes from revision #4 to #5: Added | ~~Removed~~ | ~~Chan~~ged

Definition
- In premetric spaces
- In Cauchy spaces
See also

Definition

In premetric spaces

Let $R T$ R T be a ~~Archimedean~~ directed ~~ordered~~ type ~~integral~~ ~~domain~~ , ~~with~~ and a let~~dense~~ $S$ be a~~strict order~~ $T$ , - ~~let~~ ~~$R_{+}$~~ ~~be the~~ ~~semiring?~~ ~~of positive terms in~~ ~~$R$~~ ~~, and let~~ ~~$A$~~ ~~be a~~ ~~$R_{+}$~~ -premetric space. Given a directed type $I$ , a net $a x : I \to A S$ a: x: I \to A S is a Cauchy net if

x : I \to A S ⊢ c (x) : \prod_{ϵ : R_{+} T} ‖ \sum_{N : I} \prod_{i : I} \prod_{j : I} (i \geq N) \times (j \geq N) \times (x_{i} \sim_{ϵ} x_{j}) ‖

x:I \to A S \vdash ~~c(x):\prod_{\epsilon:R_{+}}~~ c(x):\prod_{\epsilon:T} \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

~~A Cauchy sequence is a Cauchy net whose index type is the natural numbers $\mathbb{N}$ .~~

Cauchy approximations

Let $R$ be a Archimedean ordered integral domain with a dense strict order, and let $R_{+}$ be the semiring? of positive terms in $R$ . If both $T$ and $I$ are $R_{+}$ , then a net $x: R_{+} \to S$ is a Cauchy approximation if

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

In Cauchy spaces

…

Cauchy sequences

A Cauchy sequence is a Cauchy net whose index type is the natural numbers $\mathbb{N}$ .