English
Let f : M → F₁ × F₂. Then ContMDiffOn I (modelWithCornersSelf 𝕜 (F₁ × F₂)) n f s is equivalent to the conjunction of ContMDiffOn for the two coordinate maps using the self-models for F₁ and F₂.
Русский
Пусть f : M → F₁ × F₂. Тогда ContMDiffOn I (modelWithCornersSelf 𝕜 (F₁ × F₂)) n f s эквивалентно двум условиям для координат fw и sw с использованием соответствующих моделей.
LaTeX
$$$\\displaystyle \\operatorname{ContMDiffOn} \\\\ I \\\\ (modelWithCornersSelf 𝕜 (F_1 \\times F_2)) \\\\ n \\\\ f \\\\ s \\iff \\operatorname{ContMDiffOn} \\\\ I \\\\ (modelWithCornersSelf 𝕜 F_1) \\\\ n \\\\ (\\mathrm{Prod.fst} \\circ f) \\\\ s \\land \\\\operatorname{ContMDiffOn} \\\\ I \\\\ (modelWithCornersSelf 𝕜 F_2) \\\\ n \\\\ (\\mathrm{Prod.snd} \\circ f) \\\\ s$$
Lean4
theorem contMDiff_prod_iff (f : M → M' × N') :
ContMDiff I (I'.prod J') n f ↔ ContMDiff I I' n (Prod.fst ∘ f) ∧ ContMDiff I J' n (Prod.snd ∘ f) :=
⟨fun h => ⟨h.fst, h.snd⟩, fun h => by convert h.1.prodMk h.2⟩
