fderiv_prodMk — Mathlib

English

If f1 and f2 are differentiable at x, then the derivative of the map x ↦ (f1 x, f2 x) is the product of their derivatives: fderiv 𝕜 (λ x, (f1 x, f2 x)) x = (fderiv 𝕜 f1 x) .prod (fderiv 𝕜 f2 x).

Русский

Если f1 и f2 дифференцируемы в точке x, то производная от отображения x ↦ (f1 x, f2 x) равна произведению их производных.

LaTeX

$$$\text{fderiv } 𝕜 (\lambda x:E, (f_1 x,f_2 x)) x = (\text{fderiv } 𝕜 f_1 x) .prod (\text{fderiv } 𝕜 f_2 x)$$$

Lean4

theorem fderiv_prodMk (hf₁ : DifferentiableAt 𝕜 f₁ x) (hf₂ : DifferentiableAt 𝕜 f₂ x) :
    fderiv 𝕜 (fun x : E => (f₁ x, f₂ x)) x = (fderiv 𝕜 f₁ x).prod (fderiv 𝕜 f₂ x) :=
  (hf₁.hasFDerivAt.prodMk hf₂.hasFDerivAt).fderiv

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