Homotopy Type Theory modulus of Cauchy convergence > history (changes)

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

Showing changes from revision #4 to #5: Added | Removed | Changed

Contents

< modulus of convergence

category: redirected to nlab

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 SS be a premetric space, and let x∈S Ix \in S^I be a net with index set II. 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∘Mx \circ M of a net xx and a modulus of Cauchy convergence MM 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 SS be a premetric space, and let x:I→Sx:I \to S be a net with index type II. A modulus of Cauchy convergence is a function M:ℚ +→IM: \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∘Mx \circ M of a net xx and a modulus of Cauchy convergence MM is also a net.

See also

References

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

EditDiscussPrevious revisionHide changesHistory (4 revisions) Print Source