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

Showing changes from revision #18 to #19: Added | Removed | Changed


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


In Archimedean ordered fields

Let FF be an Archimedean ordered field . A and function letf:FFf:F \to F is continuous at a point c:Fc:F

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

ffbe the positive elements in is FF. A function f:FFf:F \to F is pointwise continuous in FF if it is continuous at all pointscc:

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

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 June 10, 2022 at 13:37:11 by Anonymous?. See the history of this page for a list of all contributions to it.