A function f has the continuous linear map f' as derivative along the filter L if f x' = f x + f' (x' - x) + o (x' - x) when x' converges along the filter L. This definition is designed to be specialized for L = nhds x (in has_fderiv_at), giving rise to the usual notion of Fréchet derivative, and for L = nhds_within x s (in has_fderiv_within_at), giving rise to the notion of Fréchet derivative along the set s.

A function f has the continuous linear map f' as derivative at x within a set s if f x' = f x + f' (x' - x) + o (x' - x) when x' tends to x inside s.

A function f has the continuous linear map f' as derivative at x if f x' = f x + f' (x' - x) + o (x' - x) when x' tends to x.

A function f is differentiable at a point x within a set s if it admits a derivative there (possibly non-unique).

A function f is differentiable at a point x if it admits a derivative there (possibly non-unique).

If f has a derivative at x within s, then fderiv_within 𝕜 f s x is such a derivative. Otherwise, it is set to 0.

If f has a derivative at x, then fderiv 𝕜 f x is such a derivative. Otherwise, it is set to 0.

differentiable_on 𝕜 f s means that f is differentiable within s at any point of s.

differentiable 𝕜 f means that f is differentiable at any point.

If a function f has a derivative f' at x, a rescaled version of f around x converges to f', i.e., n (f (x + (1/n) v) - f x) converges to f' v. More generally, if c n tends to infinity and c n * d n tends to v, then c n * (f (x + d n) - f x) tends to f' v. This lemma expresses this fact, for functions having a derivative within a set. Its specific formulation is useful for tangent cone related discussions.

unique_diff_within_at achieves its goal: it implies the uniqueness of the derivative.

The chain rule.

The image of a tangent cone under the differential of a map is included in the tangent cone to the image.

If a set has the unique differentiability property at a point x, then the image of this set under a map with onto derivative has also the unique differentiability property at the image point.