English
For f: M → M' × N', ContMDiffAt I (I'.prod J') n f x is equivalent to ContMDiffAt I I' n (Prod.fst ∘ f) x and ContMDiffAt I J' n (Prod.snd ∘ f) x.
Русский
Для отображения f: M → M' × N' верна эквивалентность: f содержится в C^n в точке x по соответствующим картам тогда и только тогда, когда обе координаты являются C^n в x.
LaTeX
$$$\\displaystyle \\operatorname{ContMDiffAt} \\\\ I \\\\ (I'.prod J') \\\\ n \\\\ f \\\\ x \\iff (\\operatorname{ContMDiffAt} \\\\ I \\\\ I' \\\\ n \\\\ (\\mathrm{Prod.fst} \\circ f) \\\\ x) \\land (\\operatorname{ContMDiffAt} \\\\ I \\\\ J' \\\\ n \\\\ (\\mathrm{Prod.snd} \\circ f) \\\\ x)$$
Lean4
theorem contMDiff_prod_module_iff (f : M → F₁ × F₂) :
ContMDiff I 𝓘(𝕜, F₁ × F₂) n f ↔ ContMDiff I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) ∧ ContMDiff I 𝓘(𝕜, F₂) n (Prod.snd ∘ f) :=
by
rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]
exact contMDiff_prod_iff f
