Homotopy Type Theory limit of a function > history (Rev #5, changes)

Showing changes from revision #4 to #5: Added | ~~Removed~~ | ~~Chan~~ged

Definition
See also

Definition

In real rational numbers

Let $ℝ ℚ$ ~~\mathbb{R}~~ \mathbb{Q} be a the ~~type~~ of ~~real~~ rational numbers and let ${ℝ ℚ}_{+}$ ~~\mathbb{R}_{+}~~ \mathbb{Q}_{+} be the positive ~~real~~ rational numbers. Thelimit of a function $f : ℝ ℚ \to ℝ ℚ$ ~~f:\mathbb{R}~~ f:\mathbb{Q} \to ~~\mathbb{R}~~ \mathbb{Q} approaching a term $c : ℝ ℚ$ ~~c:\mathbb{R}~~ c:\mathbb{Q} is a term $L : ℝ ℚ$ ~~L:\mathbb{R}~~ L:\mathbb{Q} such that for all directed types $I$ and nets $x : I \to ℝ ℚ$ x:I \to ~~\mathbb{R}~~ \mathbb{Q} where $c$ is the limit of $x$ , $L$ is the limit of $f \circ x$ , or written in type theory:

\prod_{I:\mathcal{U}} isDirected(I) \times \prod_{x:I \to \mathbb{R}} isLimit(c, x) \times isLimit(L, f \circ x)

where

isLimit (c, x) ≔ \prod_{ϵ : {ℝ ℚ}_{+}} ‖ \sum_{N : I} \prod_{i : I} (i \geq N) \to (| x_{i} - c | < ϵ) ‖

isLimit(c,x) \coloneqq ~~\prod_{\epsilon:\mathbb{R}_{+}}~~ \prod_{\epsilon:\mathbb{Q}_{+}} \Vert \sum_{N:I} \prod_{i:I} (i \geq N) \to (\vert x_i - c \vert \lt \epsilon) \Vert

isLimit (L, f \circ x) ≔ \prod_{ϵ : {ℝ ℚ}_{+}} ‖ \sum_{N : I} \prod_{i : I} (i \geq N) \to (| f (x_{i}) - L | < ϵ) ‖

isLimit(L,f \circ x) \coloneqq ~~\prod_{\epsilon:\mathbb{R}_{+}}~~ \prod_{\epsilon:\mathbb{Q}_{+}} \Vert \sum_{N:I} \prod_{i:I} (i \geq N) \to (\vert f(x_i) - L \vert \lt \epsilon) \Vert

The limit is usually written as

L \coloneqq \lim_{x \to c} f(x)

In premetric spaces

Let $T$ be a type and let $S$ be a $T$ -premetric space and $U$ be a $V$ -premetric space. The limit of a function $f:S \to U$ approaching a term $c:S$ is a term $L:U$ such that for all directed types $I$ and nets $x:I \to S$ where $c$ is the limit of $x$ , $L$ is the limit of $f \circ x$ , or written in type theory:

\prod_{I:\mathcal{U}} isDirected(I) \times \prod_{x:I \to S} isLimit(c, x) \times isLimit(L, f \circ x)