English
If hh₂ is differentiable at h(x) with derivative h₂', and hh is differentiable at x with derivative h', then the derivative of the composition h₂ ∘ h at x is h₂' * h'.
Русский
Если hh₂ дифференцируема в h(x) с производной h₂', а hh дифференцируема в x с производной h', то производная композиции h₂ ∘ h в x равна h₂' * h'.
LaTeX
$$$$\\forall x:\\ DifferentiableAt 𝕜' h₂ (h x) \\land DifferentiableAt 𝕜 h x \\Rightarrow deriv(Function.comp h₂ h)(x) = deriv h₂ (h x) * deriv h x. $$$$
Lean4
protected nonrec theorem iterate {f : 𝕜 → 𝕜} {f' : 𝕜} (hf : HasDerivAt f f' x) (hx : f x = x) (n : ℕ) :
HasDerivAt f^[n] (f' ^ n) x :=
hf.iterate _
(have := hf.tendsto_nhds le_rfl;
by rwa [hx] at this)
hx n
