Homotopy Type Theory
modulus of Cauchy convergence > history (Rev #4)
Contents
Whenever editing is allowed on the nLab again, this article should be ported over there.
Definition
In set theory
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 a premetric space , and let x ∈ S I x \in S^I be a net with index set I I . A modulus of Cauchy convergence is a function M ∈ I ℚ + M \in I^{\mathbb{Q}_{+}} such that
∀ ϵ ∈ ℚ + . ∀ i ∈ I . ∀ j ∈ I . ( i ≥ M ( ϵ ) ) ∧ ( j ≥ M ( ϵ ) ) ⇒ ( x i ∼ ϵ x j ) \forall \epsilon \in \mathbb{Q}_{+}. \forall i \in I. \forall j \in I. (i \geq M(\epsilon)) \wedge (j \geq M(\epsilon)) \implies (x_i \sim_{\epsilon} x_j)
The composition x ∘ M x \circ M of a net x x and a modulus of Cauchy convergence M M is also a net .
In homotopy type theory
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 a premetric space , and let x : I → S x:I \to S be a net with index type I I . A modulus of Cauchy convergence is a function M : ℚ + → I M: \mathbb{Q}_{+} \to I with a type
μ : ∏ ϵ : ℚ + ∏ i : I ∏ j : I ( i ≥ M ( ϵ ) ) × ( j ≥ M ( ϵ ) ) → ( x i ∼ ϵ x j ) \mu:\prod_{\epsilon:\mathbb{Q}_{+}} \prod_{i:I} \prod_{j:I} (i \geq M(\epsilon)) \times (j \geq M(\epsilon)) \to (x_i \sim_{\epsilon} x_j)
The composition x ∘ M x \circ M of a net x x and a modulus of Cauchy convergence M M is also a net .
See also
References
Revision on April 14, 2022 at 00:08:06 by
Anonymous? .
See the history of this page for a list of all contributions to it.