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

Showing changes from revision #18 to #19: Added | Removed | Changed

# Contents

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

## Definition

### In Archimedean ordered fields

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

 isContinuousAt(f, F_{+} c) \coloneqq \prod_{\epsilon:(0, \sum_{a:F} \infty)} 0 \prod_{x:F} \lt \left[\sum_{\delta:(0, a \infty)} \left[\sum_{a:(-\delta, \delta)} x - c = a\right] \to \left[\sum_{b:(-\epsilon, \epsilon)} f(x) - f(c) = b\right]\right]

$f$be the positive elements in is $F$. A function $f:F \to F$ is pointwise continuous in $F$ if it is continuous at all points$c$:

 isPointwiseContinuous(f) \coloneqq \prod_{c:F} \prod_{x:F} isContinuousAt(f, \prod_{\epsilon:F_{+}} c) \prod_{y:F} \Vert \sum_{\delta:F_{+}} (\vert x - y \vert \lt \delta) \to (\vert f(x) - f(y) \vert \lt \epsilon) \Vert

### In preconvergence spaces

Let $S$ and $T$ be preconvergence spaces. 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} isLimit_S(x, c) \to isLimit_T(f \circ x, f(c))$

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

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

### In function limit spaces

Let $T$ be a function limit space, and let $S \subseteq T$ be a subtype of $T$. A function $f:S \to T$ is continuous at a point $c:S$ if the limit of $f$ approaching $c$ is equal to $f(c)$.

$p:\lim_{x \to c} f(x) = f(c)$

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

$p:\prod_{c:S} \lim_{x \to c} f(x) = f(c)$

The type of all pointwise continuous functions on a subtype $S$ of $T$ is defined as

$C^0(S, T) \coloneqq \sum_{f:S \to T} \prod_{c:S} \lim_{x \to c} f(x) = f(c)$