Homotopy Type Theory
limit of a function > history (Rev #2)
Contents
Definition
In premetric spaces
Let T T be a type and let S S be a T T -premetric space . The limit of a function f : S → S f:S \to S approaching a term c : S c:S is a term L : S L:S such that for all directed type s I I and net s x : I → S x:I \to S where c c is the limit of x x , L L is the limit of f ∘ x f \circ x , or written in type theory:
∏ I : 𝒰 isDirected ( I ) × ∏ x : I → S isLimit ( c , x ) × isLimit ( L , f ∘ x ) \prod_{I:\mathcal{U}} isDirected(I) \times \prod_{x:I \to S} isLimit(c, x) \times isLimit(L, f \circ x)
where
isLimit ( c , x ) ≔ ∏ ϵ : T ‖ ∑ N : I ∏ i : I ( i ≥ N ) → ( x i ∼ ϵ c ) ‖ isLimit(c,x) \coloneqq \prod_{\epsilon:T} \Vert \sum_{N:I} \prod_{i:I} (i \geq N) \to (x_i \sim_\epsilon c) \Vert
The limit is usually written as
L ≔ lim x → c f ( x ) L \coloneqq \lim_{x \to c} f(x)
In convergence spaces
…
See also
Revision on March 21, 2022 at 03:08:34 by
Anonymous? .
See the history of this page for a list of all contributions to it.