English
If φ_i are differentiable at x for all i, then the derivative of the Pi-map x ↦ φ_i(x) is the pi of the derivatives: fderiv 𝕜 (λ x,i, φ_i(x)) x = π i fderiv 𝕜 (φ_i) x.
Русский
Если для всех i отображение φ_i дифференцируемо в x, то производная от x ↦ φ_i(x) равна π(финальные производные).
LaTeX
$$$\\operatorname{fderiv}_{\\mathbb{K}}(\\lambda x,i.\\phi_i(x))\\;x = \\operatorname{ContinuousLinearMap.pi}(\\lambda i. \\operatorname{fderiv}_{\\mathbb{K}}(\\phi_i)\\;x)$$$
Lean4
theorem fderiv_pi (h : ∀ i, DifferentiableAt 𝕜 (φ i) x) :
fderiv 𝕜 (fun x i => φ i x) x = pi fun i => fderiv 𝕜 (φ i) x :=
(hasFDerivAt_pi.2 fun i => (h i).hasFDerivAt).fderiv
