Homotopy Type Theory limit of a sequence > history (Rev #3)

Contents

Definition

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

See also

Revision on June 15, 2022 at 22:55:28 by Anonymous?. See the history of this page for a list of all contributions to it.