comp — Mathlib

English

The chain rule holds under iteration for strict derivatives: (h₂ ∘ h)′(x) = h₂′(h(x)) · h′(x) when h₂ is differentiable at h(x) and h is differentiable at x.

Русский

Цепное правило справедливо и для повторной композиции в случае строгой производной: (h₂ ∘ h)′(x) = h₂′(h(x)) · h′(x).

LaTeX

$$$$\\forall x:\\; \\text{HasStrictDerivAt}(h,h',x) \\land \\text{HasStrictDerivAt}(h_2,h_2',h(x)) \\Rightarrow \\text{HasStrictDerivAt}(h_2\\circ h,(h_2'\\cdot h'),x). $$$$

Lean4

theorem comp (hh₂ : HasStrictDerivAt h₂ h₂' (h x)) (hh : HasStrictDerivAt h h' x) :
    HasStrictDerivAt (h₂ ∘ h) (h₂' * h') x := by
  rw [mul_comm]
  exact hh₂.scomp x hh

Похожие утверждения