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 FF , a functionpointwise continuous functionf:FFf:F \to F isf: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<max|(h , |h)<δ 0 \lt \max(h, \vert -h) 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 15:48:15 by Anonymous?. See the history of this page for a list of all contributions to it.