Homotopy Type Theory Cauchy net > history (changes)

Showing changes from revision #13 to #14: Added | Removed | Changed

<Cauchy net

Contents

Whenever editing is allowed on the 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

+{x|0<x}\mathbb{Q}_{+} \coloneqq \{x \in \mathbb{Q} \vert 0 \lt x\}

be the positive rational numbers. Let SS be an premetric space. A net xS Ix \in S^I is a Cauchy net if

ϵ +.NI.iI.jI.(iN)(jN)(x i ϵx j)\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

+{x|0<x}\mathbb{Q}_{+} \coloneqq \{x \in \mathbb{Q} \vert 0 \lt x\}

be the positive rational numbers.

A net xS +x \in S^{\mathbb{Q}_{+}} is a Cauchy approximation if

δ +.η +.x δ δ+ηx η\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 +N \in \mathbb{Q}_{+} defined as Nδη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

+ x:0<x\mathbb{Q}_{+} \coloneqq \sum_{x:\mathbb{Q}} 0 \lt x

be the positive rational numbers. Let SS be an premetric space. A net x:ISx: I \to S is a Cauchy net if

x:ISc(x): ϵ: + N:I i:I j:I(iN)×(jN)×(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 \mathbb{Q} be the rational numbers and let

+ x:0<x\mathbb{Q}_{+} \coloneqq \sum_{x:\mathbb{Q}} 0 \lt x

be the positive rational numbers.

A net x: +Sx: \mathbb{Q}_{+} \to S is a Cauchy approximation if

x: +Sc(x): δ: + η: +x δ δ+ηx η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: +N:\mathbb{Q}_{+} defined as Nδη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

Last revised on June 10, 2022 at 00:49:54. See the history of this page for a list of all contributions to it.