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

Contents

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. A function f:FFf:F \to F is continuous at a point c:Fc:F

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]

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.