Homotopy Type Theory pointwise continuous function > history (Rev #18, changes)

Showing changes from revision #17 to #18: 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. A function f:FFf:F \to F is continuous at a point c:Fc:F

Let FF be an Archimedean ordered field and let

isContinuousAt(f,c) ϵ:(0,) x:F[ δ:(0,)[ a:(δ,δ)xc=a][ b:(ϵ,ϵ)f(x)f(c)=b]]isContinuousAt(f, c) \coloneqq \prod_{\epsilon:(0, \infty)} \prod_{x:F} \left[\sum_{\delta:(0, \infty)} \left[\sum_{a:(-\delta, \delta)} x - c = a\right] \to \left[\sum_{b:(-\epsilon, \epsilon)} f(x) - f(c) = b\right]\right]
F +{aF|0<aF_{+} \coloneqq \{a \in F \vert 0 \lt a

ff is pointwise continuous in FF if it is continuous at all points cc:

be the positive elements in FF. A function fF Ff \in F^F is continuous at a point cFc \in F if

isPointwiseContinuous(f) c:FisContinuousAt(f,c)isPointwiseContinuous(f) \coloneqq \prod_{c:F} isContinuousAt(f, c)
isContinuousAt(f,c)ϵF +.xF.δF +.(|xc|<δ)(|f(x)f(c)|<ϵ)isContinuousAt(f, c) \coloneqq \forall \epsilon \in F_{+}. \forall x \in F. \exists \delta \in F_{+}. (\vert x - c \vert \lt \delta) \to (\vert f(x) - f(c) \vert \lt \epsilon)

In preconvergence spaces

ffLet is SSpointwise continuous and in TTFF be if it is continuous at all points preconvergence spaceccs. A function :f:STf:S \to T is continuous at a point c:Sc:S

isPointwiseContinuous isContinuousAt(f,c) I:𝒰isDirected(I)× x:ISisLimit S(x,c )FisContinuousAtisLimit T(fx,f(c)) isPointwiseContinuous(f) \coloneqq \forall c \in F isContinuousAt(f, c) \coloneqq \sum_{I:\mathcal{U}} isDirected(I) \times \prod_{x:I \to S} isLimit_S(x, c) \to isLimit_T(f \circ x, f(c))

In preconvergence spaces

ff is pointwise continuous if it is continuous at all points cc:

Let SS and TT be preconvergence spaces. A function fT Sf \in T^S is continuous at a point cSc \in S if

isPointwiseContinuous(f) c:SisContinuousAt(f,c)isPointwiseContinuous(f) \coloneqq \prod_{c:S} isContinuousAt(f, c)
isContinuousAt(f,c)IDirectedSet 𝒰.xS I.isLimit S(x,c)isLimit T(fx,f(c))isContinuousAt(f, c) \coloneqq \forall I \in DirectedSet_\mathcal{U}. \forall x \in S^I. isLimit_S(x, c) \to isLimit_T(f \circ x, f(c))

In function limit spaces

ffLet is TTpointwise continuous be a if it is continuous at all points function limit spacecc, and let :STS \subseteq T be a subtype of TT. A function f:STf:S \to T is continuous at a point c:Sc:S if the limit of $f$ approaching $c$ is equal to f(c)f(c).

isPointwiseContinuous p ( :lim xcf)cSisContinuousAt(x)=f , (c) isPointwiseContinuous(f) p:\lim_{x \coloneqq \to \forall c} c f(x) \in = S f(c) isContinuousAt(f, c)

In homotopy type theory

ff is pointwise continuous on SS if it is continuous at all points c:Sc:S:

In Archimedean ordered fields

p: c:Slim xcf(x)=f(c)p:\prod_{c:S} \lim_{x \to c} f(x) = f(c)

Let The type of all pointwise continuous functions on a subtype F S F S be of anArchimedean ordered fieldTT and is let defined as

F +C 0(S,T) f:STa:F c:S0lim xc<fa(x)=f(c) F_{+} C^0(S, T) \coloneqq \sum{a:F} \sum_{f:S 0 \to \lt T} a \prod_{c:S} \lim_{x \to c} f(x) = f(c)

be the positive elements in FF. A function f:FFf:F \to F is continuous at a point c:Fc:F

isContinuousAt(f,c) ϵ:F + x:F δ:F +(|xc|<δ)(|f(x)f(c)|<ϵ)isContinuousAt(f, c) \coloneqq \prod_{\epsilon:F_{+}} \prod_{x:F} \Vert \sum_{\delta:F_{+}} (\vert x - c \vert \lt \delta) \to (\vert f(x) - f(c) \vert \lt \epsilon) \Vert

ff is pointwise continuous in FF if it is continuous at all points cc:

isPointwiseContinuous(f) c:FisContinuousAt(f,c)isPointwiseContinuous(f) \coloneqq \prod_{c:F} isContinuousAt(f, c)

In preconvergence spaces

Let SS and TT be preconvergence spaces. A function f:STf:S \to T is continuous at a point c:Sc:S

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

ff is pointwise continuous if it is continuous at all points cc:

isPointwiseContinuous(f) c:SisContinuousAt(f,c)isPointwiseContinuous(f) \coloneqq \prod_{c:S} isContinuousAt(f, c)

In function limit spaces

Let TT be a function limit space, and let STS \subseteq T be a subtype of TT. A function f:STf:S \to T is continuous at a point c:Sc:S if the limit of $f$ approaching $c$ is equal to f(c)f(c).

p:lim xcf(x)=f(c)p:\lim_{x \to c} f(x) = f(c)

ff is pointwise continuous on SS if it is continuous at all points c:Sc:S:

p: c:Slim xcf(x)=f(c)p:\prod_{c:S} \lim_{x \to c} f(x) = f(c)

The type of all pointwise continuous functions on a subtype SS of TT is defined as

C 0(S,T) f:ST c:Slim xcf(x)=f(c)C^0(S, T) \coloneqq \sum_{f:S \to T} \prod_{c:S} \lim_{x \to c} f(x) = f(c)

See also

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