Homotopy Type Theory differentiable function > history (changes)

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

Contents

Definition

Given an Archimedean ordered field FF, a function f:FFf:F \to F is pointwise differentiable if it comes with a function D(f):FFD(f):F \to F called the derivative and such that for every positive element ϵ:F +\epsilon:F_+, there exists a positive element δ:F +\delta:F_+ such that for every element h:Fh:F such that 0<|h|<δ0 \lt \vert h \vert \lt \delta and for every element x:Fx:F,

|f(x+h)f(x)hD(f)(x)|<ϵ\vert f(x + h) - f(x) - h D(f)(x) \vert \lt \epsilon

See also

Last revised on June 11, 2022 at 00:26:25. See the history of this page for a list of all contributions to it.