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

Skip the Navigation Links | Home Page | All Pages | Latest Revisions | Authors |

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

Contents

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

Definition

In set Archimedean theory ordered fields

In Archimedean ordered fields

Let FF be an Archimedean ordered field. The limit of a function f:F→Ff:\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:I→Fx:I \to F where cc is the limit of xx, LL is the limit of f∘xf \circ x, or written in type theory:

Let FF be an Archimedean ordered field and let

∏ I:𝒰isDirected(I)×∏ x:I→FisLimit(c,x)×isLimit(L,f∘x)\prod_{I:\mathcal{U}} isDirected(I) \times \prod_{x:I \to F} isLimit(c, x) \times isLimit(L, f \circ x)
F +≔{a∈F|0<aF_{+} \coloneqq \{a \in F \vert 0 \lt a

be the positive elements in FF. The limit of a function f∈F Ff \in F^F approaching an element c∈Fc \in F is an element L∈FL \in F such that for all directed sets II and nets x∈F Ix \in F^I where cc is the limit of xx, LL is the limit of f∘xf \circ x, or written in type theory:
∀I∈DirectedSet 𝒰.∀x∈F IisLimit(c,x)∧isLimit(L,f∘x)\forall I \in DirectedSet_\mathcal{U}. \forall x \in F^I isLimit(c, x) \wedge isLimit(L, f \circ x)

where the predicates
isLimit(c,x)≔∀ϵ∈F +.∃N∈I.∀i∈I.(i≥N)⇒(|x i−c|<ϵ)isLimit(c,x) \coloneqq \forall \epsilon \in F_{+}. \exists N \in I. \forall i\in I. (i \geq N) \implies (\vert x_i - c \vert \lt \epsilon)
isLimit(L,f∘x)≔∀ϵ∈F +.∃N∈I.∀i∈I.(i≥N)→(|f(x i)−L|<ϵ)isLimit(L,f \circ x) \coloneqq \forall \epsilon \in F_{+}. \exists N \in I. \forall i\in I. (i \geq N) \to (\vert f(x_i) - L \vert \lt \epsilon)

The limit is usually written as
L≔lim x→cf(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∈T Sf \in T^S approaching an element c∈Sc \in S is an element L∈TL \in T such that for all directed sets II and nets x∈S Ix \in S^I where cc is a limit of xx, LL is a limit of f∘xf \circ x, or written in type theory:
∀I∈DirectedSet 𝒰.∀x∈S I.isLimit S(x,c)×isLimit T(f∘x,L)\forall I \in DirectedSet_\mathcal{U}. \forall x \in S^I. isLimit_S(x, c) \times isLimit_T(f \circ x, L)

In homotopy type theory

In 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. The limit of a function f:F→Ff:\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:I→Fx:I \to F where cc is the limit of xx, LL is the limit of f∘xf \circ x, or written in type theory:
∏ I:𝒰isDirected(I)×∏ x:I→FisLimit(c,x)×isLimit(L,f∘x)\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)≔∏ ϵ:F +(0,∞)‖[∑ N:I∏ i:I(i≥N)→[∑ a:(−ϵ,ϵ)x i−c=a]]∑ N:I∏ i:I(i≥N)→(|x i−c|<ϵ)‖ isLimit(c,x) \coloneqq \prod_{\epsilon:F_{+}} \prod_{\epsilon:(0, \Vert \infty)} \sum_{N:I} \left[\sum_{N:I} \prod_{i:I} (i \geq N) \to (\vert \left[\sum_{a:(-\epsilon, \epsilon)} x_i - c \vert = \lt a\right]\right] \epsilon) \Vert
isLimit(L,f∘x)≔∏ ϵ:F +(0,∞)‖[∑ N:I∏ i:I(i≥N)→[∑ a:(−ϵ,ϵ)f(x i)−L=a]]∑ N:I∏ i:I(i≥N)→(|f(x i)−L|<ϵ)‖ isLimit(L,f \circ x) \coloneqq \prod_{\epsilon:F_{+}} \prod_{\epsilon:(0, \Vert \infty)} \sum_{N:I} \left[\sum_{N:I} \prod_{i:I} (i \geq N) \to (\vert \left[\sum_{a:(-\epsilon, \epsilon)} f(x_i) - L \vert = \lt a\right] \epsilon) \right] \Vert

The limit is usually written as

L≔lim x→cf(x)L \coloneqq \lim_{x \to c} f(x)

In preconvergence spaces

In preconvergence spaces

Let SS and TT be preconvergence spaces. The limit of a function f:S→Tf: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:I→Sx:I \to S where cc is a limit of xx, LL is a limit of f∘xf \circ x, or written in type theory:

∏ I:𝒰isDirected(I)×∏ x:I→SisLimit S(x,c)×isLimit T(f∘x,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

In function limit spaces

Let TT be a function limit space and let S⊆TS \subseteq T be a subtype of TT. The limit of a function f:S→Tf: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 x→cf(x)=L‖hasLimitApproaching(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:S→ThasLimitApproaching(f,c)FuncWithLim(S, T)(c) \coloneqq \sum_{f:S \to T} hasLimitApproaching(f, c)

See also

Revision on May 4, 2022 at 20:58:50 by Anonymous?. See the history of this page for a list of all contributions to it.

DiscussNext revision (to current)Previous revision (11 more)Current version of pageHide changesHistory (12 revisions)Rollback Source