English
Let f: M → M' × N' be a function between charted spaces. Then f is differentiable (MDifferentiable) iff both coordinate projections Prod.fst ∘ f and Prod.snd ∘ f are differentiable, with respect to their corresponding models.
Русский
Пусть f: M → M' × N' — отображение между картированными пространствами. Тогда f дифференцируемо тогда и только тогда, когда его координаты Prod.fst ∘ f и Prod.snd ∘ f дифференцируемы по соответствующим моделям.
LaTeX
$$$\text{MDifferentiable } I\,(I'.prod J')\ f \iff \big(\text{MDifferentiable } I\ I'\ (\mathrm{Prod.fst} \circ f) \land \text{MDifferentiable } I\ J'\ (\mathrm{Prod.snd} \circ f)\big)$$
Lean4
theorem mdifferentiable_prod_iff (f : M → M' × N') :
MDifferentiable I (I'.prod J') f ↔ MDifferentiable I I' (Prod.fst ∘ f) ∧ MDifferentiable I J' (Prod.snd ∘ f) :=
⟨fun h => ⟨h.fst, h.snd⟩, fun h => by convert h.1.prodMk h.2⟩
