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