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

Showing changes from revision #8 to #9: Added | ~~Removed~~ | ~~Chan~~ged

Definition
See also

Definition

In premetric spaces

Let $T R$ T R be a dense integral subdomain of the ~~directed~~ rational ~~type~~ numbers , ~~and~~ ~~let~~ $S ℚ$ S \mathbb{Q} be and a let $T R_{+}$ T R_{+} - be the positive terms of $R$ . Let $S$ be an $R_{+}$ -premetric space. Given a directed type $I$ , a net $x: I \to S$ is a Cauchy net if

x : I \to S ⊢ c (x) : \prod_{ϵ : T R_{+}} ‖ \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 S \vdash ~~c(x):\prod_{\epsilon:T}~~ 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 $A R$ A R be a dense integral subdomain of the ~~dense~~ rational numbers ~~Archimedean ordered abelian group~~ $\mathbb{Q}$ ~~with~~ and a let ~~point~~ $1 R_{+} : A$ ~~1:A~~ R_{+} ~~and~~ be a the ~~term~~ positive terms of $ζ R : 0 < 1$ ~~\zeta:~~ R 0 ~~\lt~~ 1~~. Let~~ ~~$A_{+} \coloneqq \sum_{a:A} (0 \lt a)$~~ ~~be the~~ ~~positive cone?~~ of ~~$A$~~ .

A net $x : {A R}_{+} \to S$ x: ~~A_{+}~~ R_{+} \to S is a ${A R}_{+}$ ~~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 ${A R}_{+}$ ~~A_{+}~~ R_{+}-Cauchy approximation is a Cauchy net indexed by ${A R}_{+}$ ~~A_{+}~~ R_{+}. This is because ${A R}_{+}$ ~~A_{+}~~ R_{+} is a strictly ordered type, and thus a directed type and a strictly codirected type, with $N : {A R}_{+}$ ~~N:A_{+}~~ N:R_{+} defined as $N \coloneqq \delta \otimes \eta$ for $δ : {A R}_{+}$ ~~\delta:A_{+}~~ \delta:R_{+} and $η : {A R}_{+}$ ~~\eta:A_{+}~~ \eta:R_{+}. $\epsilon:R_{+}$ is defined as $\epsilon + \delta + \eta$ .

In Cauchy spaces

…

Cauchy sequences

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