English
Let φ_i be maps E → F'_i. Then the derivative inside a set s of the Pi-map x ↦ (φ_i(x)) equals the pi of the derivatives of φ_i, i.e., fderivWithin of the Pi-map equals the product of fderivWithin φ_i.
Русский
Пусть φ_i: E → F'_i. Производная внутри множества s от отображения x ↦ (φ_i(x)) равна произведению производных φ_i.
LaTeX
$$$\\operatorname{fderivWithin}_{\\mathbb{K}}(\\lambda x,i.\\phi_i(x))\\;s\\;x = \\pi(\\lambda i. \\operatorname{fderivWithin}_{\\mathbb{K}}(\\phi_i)\\;s\\;x)$$$
Lean4
theorem fderivWithin_pi (h : ∀ i, DifferentiableWithinAt 𝕜 (φ i) s x) (hs : UniqueDiffWithinAt 𝕜 s x) :
fderivWithin 𝕜 (fun x i => φ i x) s x = pi fun i => fderivWithin 𝕜 (φ i) s x :=
(hasFDerivWithinAt_pi.2 fun i => (h i).hasFDerivWithinAt).fderivWithin hs
