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 S S be an premetric space . A net x ∈ S I x \in S^I is a Cauchy net if
∀ ϵ ∈ ℚ + . ∃ N ∈ I . ∀ i ∈ I . ∀ j ∈ I . ( i ≥ N ) ∧ ( j ≥ N ) ∧ ( 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 x ∈ S ℚ + 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 S S be an premetric space . A net x : I → S x: 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 ℚ \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 : ℚ + → S x: \mathbb{Q}_{+} \to S is a Cauchy approximation if
x : ℚ + → S ⊢ c ( 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.