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

Showing changes from revision #10 to #11: Added | Removed | Changed

Contents

Definition in cohesive homotopy type theory

Let SS and TT be types with terms

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

representing that the shapes of SS and TT are contractible. A function f:STf:S \to T is continuous if the shape of the curve CC defined by

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

in the product type S×TS \times T is contractible:

p:isContr(Π(C))p:isContr(\Pi(C))

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 02:50:17 by Anonymous?. See the history of this page for a list of all contributions to it.