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

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

Contents

Definition in cohesive homotopy type theory

In real numbers

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

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

representing that the shape of \mathbb{R} is contractible. 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 function mappingf:If:I \to \mathbb{R}, let us define the graph GG of the function mappingff as

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

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

p:isContr(Πesh(G)) p:isContr(\Pi(G)) p:isContr(\esh(G))

Between geometrically contractible types spaces

Let SS and TT be types with termsspace?s with terms

p S:isContr(Πesh(S)) p_S:isContr(\Pi(S)) p_S:isContr(\esh(S))
p T:isContr(Πesh(T)) p_T:isContr(\Pi(T)) p_T:isContr(\esh(T))

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

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

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

p:isContr(Πesh(G)) p:isContr(\Pi(G)) p:isContr(\esh(G))

Definition in homotopy type theory

In rational numbers

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}

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

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

isPointwiseContinuous(f) c:isContinuousAt(f,c)isPointwiseContinuous(f) \coloneqq \prod_{c:\mathbb{Q}} isContinuousAt(f, c)

ff is uniformly continuous in \mathbb{Q} if

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

In Archimedean ordered fields

Let FF be an Archimedean ordered field. An 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

Most general definition

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