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

Contents

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

Definition

In set theory

In Archimedean ordered fields

Let FF be an Archimedean ordered field and let

F +{aF|0<aF_{+} \coloneqq \{a \in F \vert 0 \lt a

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

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)

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

isPointwiseContinuous(f)cFisContinuousAt(f,c)isPointwiseContinuous(f) \coloneqq \forall c \in F isContinuousAt(f, c)

ff is uniformly continuous in FF if

isUniformlyContinuous(f)ϵF +.δF +.xF.yF.(x δy)(f(x) ϵf(y))isUniformlyContinuous(f) \coloneqq \forall \epsilon \in F_{+}. \exists \delta \in F_{+}. \forall x \in F. \forall y \in F. (x \sim_\delta y) \to (f(x) \sim_\epsilon f(y))

In preconvergence spaces

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

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))

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

isPointwiseContinuous(f)cSisContinuousAt(f,c)isPointwiseContinuous(f) \coloneqq \forall c \in S isContinuousAt(f, c)

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. 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)

ff is uniformly continuous in FF if

isUniformlyContinuous(f) ϵ:F + δ:F + x:F y:F(x δy)(f(x) ϵf(y))isUniformlyContinuous(f) \coloneqq \prod_{\epsilon:F_{+}} \Vert \sum_{\delta:F_{+}} \prod_{x:F} \prod_{y:F} (x \sim_\delta y) \to (f(x) \sim_\epsilon f(y)) \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 April 16, 2022 at 07:37:31 by Anonymous?. See the history of this page for a list of all contributions to it.