pointwise continuous function (changes) in nLab
Showing changes from revision #7 to #8: Added | Removed | Changed
Context
Analysis
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 c∈ℝc \in \mathbb{R} if
isContinuousAt(f,c)≔∀ϵ∈ℝ +.∃δ∈ℝ +.∀x∈ℝ.(|x−c|<δ)→(|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 +≔{a∈F|0<a}K +≔{a∈K|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:F→Kf:F \to K is continuous at a point c∈Fc \in F if
isContinuousAt(f,c)≔∀ϵ∈K +.∀x∈F.∃δ∈F +.(max(x−c,c−x)<δ)→(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)≔∀c∈F.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:X→Yf:X \to Y is continuous at a point c∈Xc \in X if
isContinuousAt(f,c)≔∀ϵ∈ℝ +.∀x∈X.∃δ∈ℝ +.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)≔∀c∈X.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:X→Yf:X \to Y is continuous at a point c∈Xc \in X if
isContinuousAt(f,c)≔∀E∈𝒰(Y).∀x∈X.∃D∈𝒰(X).x≈ Dc→f(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)≔∀c∈X.isContinuousAt(f,c)isPointwiseContinuous(f) \coloneqq \forall c \in X. isContinuousAt(f, c)
Definition
(pointwise continuous function between preconvergence generalised filter 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 generalised filter spaces. A function f:X→Yf:X \to Y is continuous at a point c∈Xc \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)≔∀c∈X.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 S⊆TS \subseteq T be a subset of TT. A function f:S→Tf:S \to T is continuous at a point c∈Sc \in S if the limit of $f$ approaching $c$ is equal to f(c)f(c).
lim x→cf(x)=f(c)\lim_{x \to c} f(x) = f(c)
ff is pointwise continuous on SS if it is continuous at all points c∈Sc \in S:
isPointwiseContinuous(f)≔∀c∈S.lim x→cf(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.
\begin{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:X→Yf: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)
\end{definition}
There exists a similar definition for uniform spaces:
\begin{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:X→Yf: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))
\end{definition}
See also
Last revised on November 18, 2024 at 13:45:48. See the history of this page for a list of all contributions to it.