Homotopy Type Theory limit of a sequence > history (Rev #1, changes)

Showing changes from revision #0 to #1: Added | Removed | Changed

Contents

Definition

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. A term l:Fl:F is a limit of a sequence x:Fx: \mathbb{N} \to F or that xx converges to ll if ll comes with a term

λ: ϵ:F + N: i:(iN)(|x il|<ϵ)\lambda: \prod_{\epsilon:F_{+}} \Vert \sum_{N:\mathbb{N}} \prod_{i:\mathbb{N}} (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:(iN)(|x il|<ϵ))\lim x \coloneqq \sum_{l:F} \left(\prod_{\epsilon:F_{+}} \Vert \sum_{N:\mathbb{N}} \prod_{i:\mathbb{N}} (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 xa(x)\lim_{x \to \infty} a(x)

For sequential convergence spaces

Let SS be a sequential convergence space. A term l:Sl:S is a limit of a sequence x:Sx: \mathbb{N} \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:35:58 by Anonymous?. See the history of this page for a list of all contributions to it.