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

Showing changes from revision #13 to #14: Added | Removed | Changed

Contents

Definition in cohesive homotopy type theory

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

In real numbers

Definition

Let \mathbb{R} be the (two-sided) Dedekind real numbers with a term

In set theory

p :isContr(esh())p_\mathbb{R}:isContr(\esh(\mathbb{R}))

In Archimedean ordered fields

representing Let that theshapeFF of be an\mathbb{R}Archimedean ordered field is and letcontractible. and let II be a closed interval or open interval in \mathbb{R}. Because the shape of \mathbb{R} is contractible, the shape of any closed or open interval in \mathbb{R} is contractible. Given a mapping f:If:I \to \mathbb{R}, let us define the graph GG of the mapping ff as

GF + x:I{(ax,Ff|(0x<)a) G F_{+} \coloneqq \sum_{x:I} \{a (x, \in f(x)) F \vert 0 \lt a

in be the product positive type elements in I F× I F \times \mathbb{R} . A functionfF F f \in F^F is continuous at a point if the shape of G cF G c \in F is if contractible:

p isContinuousAt:isContr(eshf,c)ϵF +.xF.δF +.(G|xc|<δ)(|f(x)f(c)|<ϵ) p:isContr(\esh(G)) 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)

Between geometrically contractible spaces

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

Let SS and TT be space?s with terms

isPointwiseContinuous(f)cFisContinuousAt(f,c)isPointwiseContinuous(f) \coloneqq \forall c \in F isContinuousAt(f, c)
p S:isContr(esh(S))p_S:isContr(\esh(S))

ff is uniformly continuous in FF if

p T:isContr(esh(T))p_T:isContr(\esh(T))
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))

representing that the shapes of SS and TT are contractible. Given a mapping f:STf:S \to T, let us define the graph GG of the mapping ff as

In preconvergence spaces

G x:S(x,f(x))G \coloneqq \sum_{x:S} (x, f(x))

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

in the product type I×I \times \mathbb{R}. ff is continuous if the shape of GG is contractible:

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))
p:isContr(esh(G))p:isContr(\esh(G))

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

Definition in homotopy type theory

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

In rational numbers

In homotopy type theory

Let \mathbb{Q} be the rational numbers. An function f:f:\mathbb{Q} \to \mathbb{Q} is continuous at a point c:c:\mathbb{Q}

In Archimedean ordered fields

isContinuousAt(f,c) ϵ: + x: δ: +(|xc|<δ)(|f(x)f(c)|<ϵ)isContinuousAt(f, c) \coloneqq \prod_{\epsilon:\mathbb{Q}_{+}} \prod_{x:\mathbb{Q}} \Vert \sum_{\delta:\mathbb{Q}_{+}} (\vert x - c \vert \lt \delta) \to (\vert f(x) - f(c) \vert \lt \epsilon) \Vert

Let FF be an Archimedean ordered field and let

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

F +a:F0<aF_{+} \coloneqq \sum{a:F} 0 \lt a
isPointwiseContinuous(f) c:isContinuousAt(f,c)isPointwiseContinuous(f) \coloneqq \prod_{c:\mathbb{Q}} isContinuousAt(f, c)

be the positive elements in FF. A function f:FFf:F \to F is continuous at a point c:Fc:F

ff is uniformly continuous in \mathbb{Q} if

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
isUniformlyContinuous(f) ϵ: + δ: + x: y:(x δy)(f(x) ϵf(y))isUniformlyContinuous(f) \coloneqq \prod_{\epsilon:\mathbb{Q}_{+}} \Vert \sum_{\delta:\mathbb{Q}_{+}} \prod_{x:\mathbb{Q}} \prod_{y:\mathbb{Q}} (x \sim_\delta y) \to (f(x) \sim_\epsilon f(y)) \Vert

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

In Archimedean ordered fields

isPointwiseContinuous(f) c:FisContinuousAt(f,c)isPointwiseContinuous(f) \coloneqq \prod_{c:F} isContinuousAt(f, c)

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

ff is uniformly continuous in FF if

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

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

In preconvergence spaces

isPointwiseContinuous(f) c:FisContinuousAt(f,c)isPointwiseContinuous(f) \coloneqq \prod_{c:F} isContinuousAt(f, c)

Let SS and TT be preconvergence spaces. A function f:STf:S \to T is continuous at a point c:Sc:S

ff is uniformly continuous in FF if

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

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

Most general definition

isPointwiseContinuous(f) c:SisContinuousAt(f,c)isPointwiseContinuous(f) \coloneqq \prod_{c:S} isContinuousAt(f, c)

Let SS be a type with a predicate S\to_S between the type of all nets in SS

I:𝒰isDirected(I)×(IS)\sum_{I:\mathcal{U}} isDirected(I) \times (I \to S)

and SS itself, and let TT be a type with a predicate T\to_T between the type of all nets in TT

I:𝒰isDirected(I)×(IT)\sum_{I:\mathcal{U}} isDirected(I) \times (I \to T)

and TT itself.

A function f:STf:S \to T is continuous at a point c:Sc:S

isContinuousAt(f,c) I:𝒰isDirected(I)× x:IS(x Sc)(fx Tf(c))isContinuousAt(f, c) \coloneqq \sum_{I:\mathcal{U}} isDirected(I) \times \prod_{x:I \to S} (x \to_S c) \to (f \circ x \to_T 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)

See also

Revision on April 14, 2022 at 05:40:02 by Anonymous?. See the history of this page for a list of all contributions to it.