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

Definition

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

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

$f$ is pointwise continuous in $\mathbb{Q}$ if it is continuous at all points $c$ :

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

$f$ is uniformly continuous in $\mathbb{Q}$ if

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

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

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

$f$ is pointwise continuous in $F$ if it is continuous at all points $c$ :

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

$f$ is uniformly continuous in $F$ if

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

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

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

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

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

and $T$ itself.

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

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

$f$ is pointwise continuous if it is continuous at all points $c$ :

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