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

Skip the Navigation Links | Home Page | All Pages | Latest Revisions | Authors |

Showing changes from revision #11 to #12: Added | Removed | Changed

Contents

Definition

In premetric spaces

Let R ℚ R \mathbb{Q} be a dense integral subdomain of therational numbers and letℚ\mathbb{Q} and let R +R_{+} be the positive terms of RR. Let SS be an R +R_{+}-premetric space. A net x:I→Sx: I \to S is a Cauchy net if

ℚ +≔∑ x:ℚ0<x:I→S⊢c(x):∏ ϵ:R +‖∑ N:I∏ i:I∏ j:I(i≥N)×(j≥N)×(x i∼ ϵx j)‖ x:I \mathbb{Q}_{+} \to \coloneqq S \sum_{x:\mathbb{Q}} \vdash 0 c(x):\prod_{\epsilon:R_{+}} \lt \Vert x \sum_{N:I} \prod_{i:I} \prod_{j:I} (i \geq N) \times (j \geq N) \times (x_i \sim_{\epsilon} x_j) \Vert

be the positive rational numbers. Let SS be an premetric space. A net x:I→Sx: I \to S is a Cauchy net if
x:I→S⊢c(x):∏ ϵ:ℚ +‖∑ N:I∏ i:I∏ j:I(i≥N)×(j≥N)×(x i∼ ϵx j)‖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 R ℚ R \mathbb{Q} be a dense integral subdomain of therational numbers and letℚ\mathbb{Q} and let R +R_{+} be the positive terms of RR.

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

ℚ +≔∑ x:ℚ0<x\mathbb{Q}_{+} \coloneqq \sum_{x:\mathbb{Q}} 0 \lt x
x:R +→S⊢c(x):∏ δ:R +∏ η:R +x δ∼ δ+ηx ηx:R_{+} \to S \vdash c(x):\prod_{\delta:R_{+}} \prod_{\eta:R_{+}} x_\delta \sim_{\delta + \eta} x_\eta

be the positive rational numbers.

Every A netR +x:ℚ +→S R_{+} x: \mathbb{Q}_{+} \to S - is aCauchy approximationCauchy approximation is if a Cauchy net indexed byR +R_{+}. This is because R +R_{+} is a strictly ordered type, and thus a directed type and a strictly codirected type, with N:R +N:R_{+} defined as N≔δ⊗ηN \coloneqq \delta \otimes \eta for δ:R +\delta:R_{+} and η:R +\eta:R_{+}. ϵ:R +\epsilon:R_{+} is defined as ϵ≔δ+η\epsilon \coloneqq \delta + \eta.

x:ℚ +→S⊢c(x):∏ δ:R +∏ η:R +x δ∼ δ+ηx ηx:\mathbb{Q}_{+} \to S \vdash c(x):\prod_{\delta:R_{+}} \prod_{\eta:R_{+}} 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:ℚ +N:\mathbb{Q}_{+} defined as N≔δ⊗ηN \coloneqq \delta \otimes \eta for δ:Rℚ +\delta:R\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

Revision on April 14, 2022 at 00:03:39 by Anonymous?. See the history of this page for a list of all contributions to it.

DiscussNext revision (2 more)Previous revision (11 more)Current version of pageHide changesHistory (13 revisions)Rollback Source