# Homotopy Type Theory differentiable function > history (Rev #7, changes)

Showing changes from revision #6 to #7: Added | Removed | Changed

# Contents

## Definition

Given an Archimedean ordered field $F$ , a functionpointwise continuous function$f:F \to F$ is$f:F \to F$ is pointwise differentiable if it comes with a function $D(f):F \to F$ called the derivative and such that for every positive element $\epsilon:F_+$, there exists a positive element $\delta:F_+$ such that for every element $h:F$ such that  0 \lt \max(h, \vert -h) h \vert \lt \delta and for every element $x:F$,

$\vert f(x + h) - f(x) - h D(f)(x) \vert \lt \epsilon$