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

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

Contents

Definition

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 premetric Archimedean spaces ordered fields

Let R F R F be a an dense integral subdomain of the rational Archimedean numbers ordered field . An function f:FF \mathbb{Q} f:F \to F and is letR +R_{+} be the positive terms of RR. Let SS and TT be R +R_{+}-premetric spaces. A function f:STf:S \to T is continuous at a point c: S F c:S c:F

isContinuousAt(f,c) ϵ: R F + x: S F δ: R F +(|x δc|<δ)(|f(x) ϵf(c)|<ϵ) isContinuousAt(f, c) \coloneqq \prod_{\epsilon:R_{+}} \prod_{\epsilon:F_{+}} \prod_{x:S} \prod_{x:F} \Vert \sum_{\delta:R_{+}} \sum_{\delta:F_{+}} (x (\vert \sim_\delta x c) - c \vert \lt \delta) \to (f(x) (\vert \sim_\epsilon f(x) f(c)) - f(c) \vert \lt \epsilon) \Vert

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

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

ff is uniformly continuous in FF if

isUniformlyContinuous(f) ϵ: R F + δ: R F + x: S F y: S F(x δy)(f(x) ϵf(y)) isUniformlyContinuous(f) \coloneqq \prod_{\epsilon:R_{+}} \prod_{\epsilon:F_{+}} \Vert \sum_{\delta:R_{+}} \sum_{\delta:F_{+}} \prod_{x:S} \prod_{x:F} \prod_{y:S} \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 March 31, 2022 at 15:29:41 by Anonymous?. See the history of this page for a list of all contributions to it.