English
Consider a map f: M → F1 × F2. Then f is differentiable in the module sense (MDifferentiableOn with 𝓘(𝕜, F1 × F2)) exactly when its coordinate projections are differentiable with respect to each factor, i.e., Prod.fst ∘ f and Prod.snd ∘ f are differentiable into F1 and F2 respectively.
Русский
Пусть f: M → F1 × F2. Тогда f дифференцируемо по модулю тогда и только тогда, когда проекции на первую и вторую координаты дифференцируемы.
LaTeX
$$$\text{MDifferentiable } I\,\mathcal{I}(\mathbb{K},F_1\times F_2)\ f \iff \big(\text{MDifferentiable } I\mathcal{I}(\mathbb{K},F_1)\ (\mathrm{Prod.fst} \circ f) \land \text{MDifferentiable } I\mathcal{I}(\mathbb{K},F_2)\ (\mathrm{Prod.snd} \circ f)\big)$$
Lean4
theorem mdifferentiable_prod_module_iff (f : M → F₁ × F₂) :
MDifferentiable I 𝓘(𝕜, F₁ × F₂) f ↔
MDifferentiable I 𝓘(𝕜, F₁) (Prod.fst ∘ f) ∧ MDifferentiable I 𝓘(𝕜, F₂) (Prod.snd ∘ f) :=
by
rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]
exact mdifferentiable_prod_iff f
