Homotopy Type Theory limit of a net > history (Rev #14, changes)

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

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

Contents

Whenever editing is allowed on the nLab again, this article should be ported over there.

Definition

In rational set numbers theory

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

For Archimedean ordered fields

λ:∏ ϵ:ℚ +‖∑ 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

Let FF be an Archimedean ordered field and let
F +≔{a∈F|0<aF_{+} \coloneqq \{a \in F \vert 0 \lt a

be the positive elements in FF. Given a directed type II, an element l∈Fl \in F is a limit of a net x∈F Ix \in F^I or that xx converges to ll if
∀ϵ∈F +.∃N∈I.∀i∈I.(i≥N)→(|x i−l|<ϵ)\forall \epsilon \in F_{+}. \exists N \in I. \forall i \in I. (i \geq N) \to (\vert x_i - l \vert \lt \epsilon)

The set 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 \{ l \in F \vert \forall \epsilon \in F_{+}. \exists N \in I. \forall i \in I. (i \geq N) \to (\vert x_i - l \vert \lt \epsilon) \}

A limit of a sequence a∈F ℕa \in F^\mathbb{N} is usually written as
lim x→∞a(x)\lim_{x \to \infty} a(x)

For preconvergence spaces

Let SS be a preconvergence space. Given a directed type II, an element l∈Sl \in S is a limit of a net x∈S Ix \in S^I or that xx converges to ll if isLimit S(x,l)isLimit_S(x, l).

The set of all limits of a net is defined as
limx≔{l∈S|isLimit S(x,l)}\lim x \coloneqq \{l\in S \vert isLimit_S(x, l) \}

In homotopy type theory

For Archimedean ordered fields

Let FF be an Archimedean ordered field and let
F +≔∑a:F0<aF_{+} \coloneqq \sum{a:F} 0 \lt a

be the positive elements in FF. 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:\mathbb{Q}} \sum_{l:F} \left(\prod_{\epsilon:\mathbb{Q}_{+}} \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:ℕ→ ℚ F a:\mathbb{N} \to \mathbb{Q} F is usually written as

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

In Archimedean ordered fields

For preconvergence spaces

Let F S F S be an a Archimedean preconvergence ordered space field . and Given let aF +F_{+} be the type of positive rational numbers. Given a directed type II, a term l: F S l:F l:S is a limit of a net x:I→ F S x: I \to F S or that xx converges to ll if the propositionisLimit S(x,l) l isLimit_S(x, l) comes is with a termcontractible.

λ:∏ ϵ: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 S(∏ ϵ:F +‖∑ N:I∏ i:I(i≥N)→(|x i−l|<ϵ)‖)isLimit S(x,l) \lim x \coloneqq \sum_{l:F} \sum_{l:S} \left(\prod_{\epsilon:F_{+}} isLimit_S(x, \Vert l) \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 April 14, 2022 at 05:09:57 by Anonymous?. See the history of this page for a list of all contributions to it.

DiscussNext revision (3 more)Previous revision (13 more)Current version of pageHide changesHistory (16 revisions)Rollback Source