Homotopy Type Theory limit of a net > history (Rev #13)

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

Contents

Definition

In rational numbers

Let ℚ\mathbb{Q} be the rational numbers and let ℚ +\mathbb{Q}_{+} be the type of positive rational numbers. Given a directed type II, a term l:ℚl:\mathbb{Q} is a limit of a net x:I→ℚx: I \to \mathbb{Q} or that xx converges to ll if ll comes with a term

λ:∏ ϵ:ℚ +‖∑ N:I∏ i:I(i≥N)→(|x i−l|<ϵ)‖\lambda: \prod_{\epsilon:\mathbb{Q}_{+}} \Vert \sum_{N:I} \prod_{i:I} (i \geq N) \to (\vert x_i - l \vert \lt \epsilon) \Vert

The type of all limits of a net is defined as

limx≔∑ l:ℚ(∏ ϵ:ℚ +‖∑ N:I∏ i:I(i≥N)→(|x i−l|<ϵ)‖)\lim x \coloneqq \sum_{l:\mathbb{Q}} \left(\prod_{\epsilon:\mathbb{Q}_{+}} \Vert \sum_{N:I} \prod_{i:I} (i \geq N) \to (\vert x_i - l \vert \lt \epsilon) \Vert\right)

A limit of a sequence a:ℕ→ℚa:\mathbb{N} \to \mathbb{Q} is usually written as

lim x→∞a(x)\lim_{x \to \infty} a(x)

In Archimedean ordered fields

Let FF be an Archimedean ordered field and let F +F_{+} be the type of positive rational numbers. Given a directed type II, a term l:Fl:F is a limit of a net x:I→Fx: I \to F or that xx converges to ll if ll comes with a term

λ:∏ ϵ:F +‖∑ N:I∏ i:I(i≥N)→(|x i−l|<ϵ)‖\lambda: \prod_{\epsilon:F_{+}} \Vert \sum_{N:I} \prod_{i:I} (i \geq N) \to (\vert x_i - l \vert \lt \epsilon) \Vert

The type of all limits of a net is defined as

limx≔∑ l:F(∏ ϵ:F +‖∑ N:I∏ i:I(i≥N)→(|x i−l|<ϵ)‖)\lim x \coloneqq \sum_{l:F} \left(\prod_{\epsilon:F_{+}} \Vert \sum_{N:I} \prod_{i:I} (i \geq N) \to (\vert x_i - l \vert \lt \epsilon) \Vert\right)

A limit of a sequence a:ℕ→Fa:\mathbb{N} \to F is usually written as

lim x→∞a(x)\lim_{x \to \infty} a(x)

Most general definition

Let SS be a type with a predicate →\to between the type of all nets in SS

∑ I:𝒰isDirected(I)×(I→S)\sum_{I:\mathcal{U}} isDirected(I) \times (I \to S)

and SS itself.

Given a directed type II, a term l:Sl:S is a limit of a net x:I→Sx: I \to S or that xx converges to ll if the proposition x→lx \to l is contractible.

The type of all limits of a net is defined as

limx≔∑ l:Sx→l\lim x \coloneqq \sum_{l:S} x \to l

See also

Revision on March 31, 2022 at 16:02:40 by Anonymous?. See the history of this page for a list of all contributions to it.

DiscussNext revision (4 more)Previous revision (12 more)Current version of pageChanges from previous revisionHistory (16 revisions)Rollback Source