nLab pointwise continuous function

Contents

Contents

Idea

The concept of continuous functions familiar from epsilontic analysis.

Definition

Definition

(pointwise continuous function in the real numbers)

Let \mathbb{R} be the real numbers and let

+{a|0<a}\mathbb{R}_{+} \coloneqq \{a \in \mathbb{R} \vert 0 \lt a\}

be the positive elements in \mathbb{R}. A function f:f:\mathbb{R} \to \mathbb{R} is continuous at a point cc \in \mathbb{R} if

isContinuousAt(f,c)ϵ +.δ +.x.(|xc|<δ)(|f(x)f(c)|<ϵ)isContinuousAt(f, c) \coloneqq \forall \epsilon \in \mathbb{R}_{+}. \exists \delta \in \mathbb{R}_{+}. \forall x \in \mathbb{R}. (\vert x - c \vert \lt \delta) \to (\vert f(x) - f(c) \vert \lt \epsilon)

ff is pointwise continuous in \mathbb{R} if it is continuous at all points cc:

isPointwiseContinuous(f)c.isContinuousAt(f,c)isPointwiseContinuous(f) \coloneqq \forall c \in \mathbb{R}. isContinuousAt(f, c)
Definition

(pointwise continuous function between Archimedean ordered fields)

Let FF and KK be Archimedean ordered fields and let

F +{aF|0<a}K +{aK|0<a}F_{+} \coloneqq \{a \in F \vert 0 \lt a\} \quad K_{+} \coloneqq \{a \in K \vert 0 \lt a\}

be the positive elements in FF and KK. A function f:FKf:F \to K is continuous at a point cFc \in F if

isContinuousAt(f,c)ϵK +.xF.δF +.(max(xc,cx)<δ)(max(f(x)f(c),f(c)f(x))<ϵ)isContinuousAt(f, c) \coloneqq \forall \epsilon \in K_{+}. \forall x \in F. \exists \delta \in F_{+}. (\max(x - c, c - x) \lt \delta) \to (\max(f(x) - f(c), f(c) - f(x)) \lt \epsilon)

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

isPointwiseContinuous(f)cF.isContinuousAt(f,c)isPointwiseContinuous(f) \coloneqq \forall c \in F. isContinuousAt(f, c)
Definition

(pointwise continuous function between metric spaces)

Let (X,d X)(X, d_X) and (Y,d Y)(Y, d_Y) be metric spaces, and let

+{a|0<a}\mathbb{R}_{+} \coloneqq \{a \in \mathbb{R} \vert 0 \lt a\}

be the positive real numbers. A function f:XYf:X \to Y is continuous at a point cXc \in X if

isContinuousAt(f,c)ϵ +.xX.δ +.d X(x,c)<δd Y(f(x),f(c))<ϵ)isContinuousAt(f, c) \coloneqq \forall \epsilon \in \mathbb{R}_{+}. \forall x \in X. \exists \delta \in \mathbb{R}_{+}. d_X(x, c) \lt \delta \to d_Y(f(x), f(c)) \lt \epsilon)

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

isPointwiseContinuous(f)cX.isContinuousAt(f,c)isPointwiseContinuous(f) \coloneqq \forall c \in X. isContinuousAt(f, c)
Definition

(pointwise continuous function between uniform spaces)

Let (X,𝒰(X),)(X, \mathcal{U}(X), \approx) and (Y,𝒰(Y),)(Y, \mathcal{U}(Y), \approx) be uniform spaces. A function f:XYf:X \to Y is continuous at a point cXc \in X if

isContinuousAt(f,c)E𝒰(Y).xX.D𝒰(X).x Dcf(x) Ef(c))isContinuousAt(f, c) \coloneqq \forall E \in \mathcal{U}(Y). \forall x \in X. \exists D \in \mathcal{U}(X). x \approx_D c \to f(x) \approx_E f(c))

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

isPointwiseContinuous(f)cX.isContinuousAt(f,c)isPointwiseContinuous(f) \coloneqq \forall c \in X. isContinuousAt(f, c)
Definition

(pointwise continuous function between preconvergence spaces)

Let (X,(X),isLimit X)(X, \mathcal{F}(X), \mathrm{isLimit}_X) and (Y,(Y),isLimit Y)(Y, \mathcal{F}(Y), \mathrm{isLimit}_Y) be preconvergence spaces. A function f:XYf:X \to Y is continuous at a point cXc \in X if

isContinuousAt(f,c)F(X).isLimit X(F,c)isLimit Y(f(F),f(c)))isContinuousAt(f, c) \coloneqq \forall F \in \mathcal{F}(X).\mathrm{isLimit}_X(F, c) \to \mathrm{isLimit}_Y(f(F), f(c)))

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

isPointwiseContinuous(f)cX.isContinuousAt(f,c)isPointwiseContinuous(f) \coloneqq \forall c \in X. isContinuousAt(f, c)
Definition

(pointwise continuous function in function limit spaces)

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

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

ff is pointwise continuous on SS if it is continuous at all points cSc \in S:

isPointwiseContinuous(f)cS.lim xcf(x)=f(c)isPointwiseContinuous(f) \coloneqq \forall c \in S. \lim_{x \to c} f(x) = f(c)

As structure

In dependent type theory, one could change the universal quantifiers and existential quantifiers in the definition of uniformly continuous function into dependent product types and dependent sum types.

Definition

Let R + x:ϵ>0\mathrm{R}_+ \coloneqq \sum_{x:\mathbb{R}} \epsilon \gt 0 denote the positive real numbers. Given metric spaces (X,d X)(X, d_X) and (Y,d Y)(Y, d_Y), a pointwise continuous function between XX and YY is a function f:XYf:X \to Y between their underlying sets with a dependent function which says:

For all elements a:Xa:X and for all positive real number ϵ>0\epsilon \gt 0, there is as structure a positive real number δ>0\delta \gt 0 such that for all elements b:Xb:X, δ Y(f(a),f(b))\delta_Y(f(a), f(b)) is less than ϵ\epsilon whenever δ X(a,b)\delta_X(a, b) is less than δ\delta

a:X ϵ:R + δ: + b:X(δ X(a,b)<δ)(δ Y(f(a),f(b))<ϵ)\prod_{a:X} \prod_{\epsilon:\mathrm{R}_+} \sum_{\delta:\mathbb{R}_+} \prod_{b:X} (\delta_X(a, b) \lt \delta) \to (\delta_Y(f(a), f(b)) \lt \epsilon)

By the type theoretic axiom of choice, which is simply the distributivity of dependent function types over dependent sum types, this is the same as saying that

There exists as structure a function ω:X(R +R +)\omega:X \to (\mathrm{R}_+ \to \mathrm{R}_+) such that for all elements a:Xa:X, for all positive real numbers ϵ>0\epsilon \gt 0 and for all elements b:Xb:X, δ Y(f(a),f(b))\delta_Y(f(a), f(b)) is less than ϵ\epsilon whenever δ X(a,b)\delta_X(a, b) is less than ω(ϵ)\omega(\epsilon)

ω:X(R +R +) a:X ϵ:R + b:X(δ X(a,b)<ω(ϵ))(δ Y(f(a),f(b))<ϵ)\sum_{\omega:X \to (\mathrm{R}_+ \to \mathrm{R}_+)} \prod_{a:X} \prod_{\epsilon:\mathrm{R}_+} \prod_{b:X} (\delta_X(a, b) \lt \omega(\epsilon)) \to (\delta_Y(f(a), f(b)) \lt \epsilon)

There exists a similar definition for uniform spaces:

Definition

Given uniform spaces (X,𝒰(X),)(X, \mathcal{U}(X), \approx) and (Y,𝒰(Y),)(Y, \mathcal{U}(Y), \approx), a pointwise continuous function between XX and YY is a function f:XYf:X \to Y with a dependent function which says:

For all elements x:Ax:A and for all entourages E:𝒰(Y)E:\mathcal{U}(Y), there is as structure an entourage D:𝒰(X)D:\mathcal{U}(X) such that for all elements b:Xb:X, f(a) Ef(b)f(a) \approx_{E} f(b) whenever a Dba \approx_{D} b

a:X E:𝒰(Y) D:𝒰(X) b:X(a Db)(f(a) Ef(b))\prod_{a:X} \prod_{E:\mathcal{U}(Y)} \sum_{D:\mathcal{U}(X)} \prod_{b:X} (a \approx_{D} b) \to (f(a) \approx_{E} f(b))

By the type theoretic axiom of choice, which is simply the distributivity of dependent function types over dependent sum types, this is the same as saying that

There exists as structure a function ω:X(𝒰(Y)𝒰(X))\omega:X \to (\mathcal{U}(Y) \to \mathcal{U}(X)) between the sets of entourages such that for all elements a:Xa:X and entourages E:𝒰(Y)E:\mathcal{U}(Y) and for all elements b:Xb:X, f(a) Ef(b)f(a) \approx_{E} f(b) whenever a ω(E)ba \approx_{\omega(E)} b

ω:X(𝒰(Y)𝒰(X)) a:X E:𝒰(Y) b:X(a ω(a,E)b)(f(a) Ef(b))\sum_{\omega:X \to (\mathcal{U}(Y) \to \mathcal{U}(X))} \prod_{a:X} \prod_{E:\mathcal{U}(Y)} \prod_{b:X} (a \approx_{\omega(a, E)} b) \to (f(a) \approx_{E} f(b))

See also

Last revised on October 24, 2023 at 18:52:05. See the history of this page for a list of all contributions to it.