English
Let f map into a product of two normed F-spaces, f: M → F1 × F2. Then f is differentiable on s with respect to the product model I.(𝕜, F1 × F2) precisely when the first coordinate f1 = Prod.fst ∘ f is differentiable with respect to I and I′ and the second coordinate f2 = Prod.snd ∘ f is differentiable with respect to I and J′ on s.
Русский
Пусть F1, F2 - нормированные пространства над полем 𝕜. Пусть f: M → F1 × F2. Тогда дифференцируемость f на s (по произведению моделей) эквивалентна дифференцируемости проекций Prod.fst ∘ f и Prod.snd ∘ f по соответствующим моделям.
LaTeX
$$$\text{MDifferentiableOn } I\,\mathcal{I}(\mathbb{K},F_1\times F_2)\ f\ s \iff \big(\text{MDifferentiableOn } I\,\mathcal{I}(\mathbb{K},F_1)\ (\mathrm{Prod.fst} \circ f)\ s \land \text{MDifferentiableOn } I\,\mathcal{I}(\mathbb{K},F_2)\, (\mathrm{Prod.snd} \circ f)\ s\big)$$
Lean4
theorem mdifferentiableOn_prod_module_iff (f : M → F₁ × F₂) :
MDifferentiableOn I 𝓘(𝕜, F₁ × F₂) f s ↔
MDifferentiableOn I 𝓘(𝕜, F₁) (Prod.fst ∘ f) s ∧ MDifferentiableOn I 𝓘(𝕜, F₂) (Prod.snd ∘ f) s :=
by
rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]
exact mdifferentiableOn_prod_iff f
