5.1. First examples🔗

Mathlib has a theory of differential calculus. Given functions:

variable (f : ℝ → ℝ) (g : ℝ → ℝ)

Mathlib has tools as follows:

Differentiable ℝ f asks whether f is differentiable everywhere.
∀ x, HasDerivAt f (g x) x asks whether g is the derivative of f everywhere.
deriv f is the derivative of f (or zero if it is not differentiable).

We note in passing the following consistency:

example (h : Differentiable ℝ f) (x : ℝ) :
    HasDerivAt f (deriv f x) x :=
  (h x).hasDerivAt