theorem
differentiable_at_iff_limit_exists
(f : ℝ → ℝ)
(c : ℝ)
:
DifferentiableAt ℝ f c ↔ ∃ (L : ℝ), Filter.Tendsto (fun (x : ℝ) => (f x - f c) / (x - c)) (nhdsWithin c {c}ᶜ) (nhds L)
A real function f is differentiable at c if and only if the difference quotient
(f x - f c) / (x - c) has a limit as x → c with x ≠ c.
theorem
chain_rule
(f g : ℝ → ℝ)
(c : ℝ)
(hg : DifferentiableAt ℝ g c)
(hf : DifferentiableAt ℝ f (g c))
:
Chain rule: if g is differentiable at c and f is differentiable at g c,
then the composition f ∘ g is differentiable at c and
(f ∘ g)'(c) = f'(g c) * g'(c).