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

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

Showing changes from revision #16 to #17: Added | Removed | Changed

<limit of a net

Contents

category: redirected to nlab

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

Definition

In set theory

For Archimedean ordered fields

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: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)

For preconvergence spaces

Let SS be a preconvergence space. 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 isLimit S(x,l)isLimit_S(x, l) is contractible.

The type of all limits of a net is defined as
limx≔∑ l:SisLimit S(x,l)\lim x \coloneqq \sum_{l:S} isLimit_S(x, l)

See also

Revision on June 10, 2022 at 01:44:40 by Anonymous?. See the history of this page for a list of all contributions to it.

DiscussNext revision (to current)Previous revision (16 more)Current version of pageHide changesHistory (16 revisions)Rollback Source