English
Let f be a map from a charted space M into a product space M' × N'. Then f is differentiable on a set s (in the sense of MDifferentiableOn) with respect to the product model I'.prod J' if and only if the first coordinate map Prod.fst ∘ f is differentiable on s with respect to I and I', and the second coordinate map Prod.snd ∘ f is differentiable on s with respect to I and J'.
Русский
Пусть f : M → M' × N' дана. Тогда f дифференцируема на s в смысле MDifferentiableOn для произведения моделей I.′, J′ тогда и только тогда, когда частичные проекции Prod.fst ∘ f и Prod.snd ∘ f дифференцируемы на s по I, I′ и соответственно по I, J′.
LaTeX
$$$\text{MDifferentiableOn } I\,(I'.prod J')\ f\ s \iff \big(\text{MDifferentiableOn } I\ I'\ (\mathrm{Prod.fst} \circ f)\ s \land \text{MDifferentiableOn } I\ J'\ (\mathrm{Prod.snd} \circ f)\ s\big)$$
Lean4
theorem mdifferentiableOn_prod_iff (f : M → M' × N') :
MDifferentiableOn I (I'.prod J') f s ↔
MDifferentiableOn I I' (Prod.fst ∘ f) s ∧ MDifferentiableOn I J' (Prod.snd ∘ f) s :=
⟨fun h ↦
⟨fun x hx ↦ ((mdifferentiableWithinAt_prod_iff f).1 (h x hx)).1, fun x hx ↦
((mdifferentiableWithinAt_prod_iff f).1 (h x hx)).2⟩,
fun h x hx ↦ (mdifferentiableWithinAt_prod_iff f).2 ⟨h.1 x hx, h.2 x hx⟩⟩
