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

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

# Contents

## Definition

### In Archimedean ordered fields

Let $F$ be an Archimedean ordered field and let

Let $F$ be an Archimedean ordered field and let

$F_{+} \coloneqq \sum_{a:F} 0 \lt a$
$F_{+} \coloneqq \sum_{a:F} 0 \lt a$

be the positive elements in $F$. A function $f:F \to F$ is pointwise continuous in $F$ if

be the positive elements in $F$. A function $f:F \to F$ is pointwise continuous in $F$ if

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