English
Let f: M → F1 × F2. Then differentiability with respect to the model 𝓘(𝕜, F1 × F2) is equivalent to differentiability of the coordinate maps in F1 and F2.
Русский
Пусть f: M → F1 × F2. Дифференцируемость по модели 𝓘(𝕜, F1 × F2) эквивалентна дифференцируемости компонент в F1 и F2.
LaTeX
$$$\forall f: M \to F_1 \times F_2,\; MDifferentiableWithinAt?\,$$$
Lean4
theorem mfderiv_prod {f : M → M'} {g : M → M''} {x : M} (hf : MDifferentiableAt I I' f x)
(hg : MDifferentiableAt I I'' g x) :
mfderiv I (I'.prod I'') (fun x => (f x, g x)) x = (mfderiv I I' f x).prod (mfderiv I I'' g x) := by
classical
simp_rw [mfderiv, if_pos (hf.prodMk hg), if_pos hf, if_pos hg]
exact
hf.differentiableWithinAt_writtenInExtChartAt.fderivWithin_prodMk hg.differentiableWithinAt_writtenInExtChartAt
(I.uniqueDiffOn _ (mem_range_self _))
