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

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

Revision on June 10, 2022 at 19:48:15 by Anonymous?. See the history of this page for a list of all contributions to it.