English
For f: M → F₁ × F₂, ContMDiffOn I 𝓘(𝕜, F₁ × F₂) n f s is equivalent to the conjunction of ContMDiffOn for the two projections fst ∘ f and snd ∘ f on s.
Русский
Пусть f: M → F₁ × F₂. Тогда ContMDiffOn I 𝓘(𝕜, F₁ × F₂) n f s эквивалентно двум условиям для fst ∘ f и snd ∘ f на s.
LaTeX
$$$\\displaystyle \\operatorname{ContMDiffOn} \\\\ I \\\\ (I'.prod J') \\\\ n \\\\ f \\\\ s \\iff (\\operatorname{ContMDiffOn} \\\\ I \\\\ (I'.prod J') \\\\ n \\\\ (\\mathrm{Prod.fst} \\circ f) \\\\ s) \\\\land (\\operatorname{ContMDiffOn} \\\\ I \\\\ (I'.prod J') \\\\ n \\\\ (\\mathrm{Prod.snd} \\circ f) \\\\ s)$$
Lean4
theorem contMDiffOn_prod_module_iff (f : M → F₁ × F₂) :
ContMDiffOn I 𝓘(𝕜, F₁ × F₂) n f s ↔
ContMDiffOn I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) s ∧ ContMDiffOn I 𝓘(𝕜, F₂) n (Prod.snd ∘ f) s :=
by
rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]
exact contMDiffOn_prod_iff f
