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

Showing changes from revision #12 to #13: Added | Removed | Changed

Contents

< limit of a function

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

Definition

In Archimedean ordered fields

Let FF be an Archimedean ordered field. The limit of a function f:FFf:\F \to F approaching a term c:Fc:F is a term L:FL:F such that for all directed types II and nets x:IFx:I \to F where cc is the limit of xx, LL is the limit of fxf \circ x, or written in type theory:

I:𝒰isDirected(I)× x:IFisLimit(c,x)×isLimit(L,fx)\prod_{I:\mathcal{U}} isDirected(I) \times \prod_{x:I \to F} isLimit(c, x) \times isLimit(L, f \circ x)

where

isLimit(c,x) ϵ:(0,)[ N:I i:I(iN)[ a:(ϵ,ϵ)x ic=a]]isLimit(c,x) \coloneqq \prod_{\epsilon:(0, \infty)} \left[\sum_{N:I} \prod_{i:I} (i \geq N) \to \left[\sum_{a:(-\epsilon, \epsilon)} x_i - c = a\right]\right]
isLimit(L,fx) ϵ:(0,)[ N:I i:I(iN)[ a:(ϵ,ϵ)f(x i)L=a]]isLimit(L,f \circ x) \coloneqq \prod_{\epsilon:(0, \infty)} \left[\sum_{N:I} \prod_{i:I} (i \geq N) \to \left[\sum_{a:(-\epsilon, \epsilon)} f(x_i) - L = a\right] \right]

The limit is usually written as

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

In preconvergence spaces

Let SS and TT be preconvergence spaces. The limit of a function f:STf:S \to T approaching a term c:Sc:S is a term L:TL:T such that for all directed types II and nets x:ISx:I \to S where cc is a limit of xx, LL is a limit of fxf \circ x, or written in type theory:

I:𝒰isDirected(I)× x:ISisLimit S(x,c)×isLimit T(fx,L)\prod_{I:\mathcal{U}} isDirected(I) \times \prod_{x:I \to S} isLimit_S(x, c) \times isLimit_T(f \circ x, L)

In function limit spaces

Let TT be a function limit space and let STS \subseteq T be a subtype of TT. The limit of a function f:STf:S \to T approaching c:Sc:S is a term L:TL:T such that the limit of ff approaching c:Sc:S is equal to LL:

hasLimitApproaching(f,c) L:Tlim xcf(x)=LhasLimitApproaching(f, c) \coloneqq \Vert \sum_{L:T} \lim_{x \to c} f(x) = L\Vert

We define the type of functions with limits approaching cc as the dependent type

FuncWithLim(S,T)(c) f:SThasLimitApproaching(f,c)FuncWithLim(S, T)(c) \coloneqq \sum_{f:S \to T} hasLimitApproaching(f, c)

See also

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