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

Showing changes from revision #20 to #21:
Added | ~~Removed~~ | ~~Chan~~ged

# Contents

< pointwise continuous function

~~
~~## Definition

~~
~~Let $F$ be an Archimedean ordered field and let

~~
~~$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

~~
~~$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$

~~
~~## See also

~~
~~
Last revised on June 10, 2022 at 19:49:30.
See the history of this page for a list of all contributions to it.