English
If each coordinate φ x i is differentiable at x within s, then derivWithin φ s x equals the Pi of coordinate derivatives.
Русский
Если каждая координата φ x i дифференцируема в x внутри s, то derivWithin φ s x равен Pi-образу производных координат.
LaTeX
$$$\text{derivWithin }\phi s x = \lambda i. \text{derivWithin } (\lambda x. \phi x i) s x$$$
Lean4
theorem derivWithin_pi (h : ∀ i, DifferentiableWithinAt 𝕜 (fun x => φ x i) s x) :
derivWithin φ s x = fun i => derivWithin (fun x => φ x i) s x :=
by
by_cases hsx : UniqueDiffWithinAt 𝕜 s x
· exact (hasDerivWithinAt_pi.2 fun i => (h i).hasDerivWithinAt).derivWithin hsx
· simp only [derivWithin_zero_of_not_uniqueDiffWithinAt hsx, Pi.zero_def]
