English
Let f: M → M' × N'. Then f is ContMDiffAt I (I'×J') n f x iff the two coordinate maps fst ∘ f and snd ∘ f are ContMDiffAt with the corresponding charts at x.
Русский
Пусть f: M → M' × N'. Тогда f ∈ ContMDiffAt I (I'×J') n f x тогда и только тогда, когда обе координаты fst ∘ f и snd ∘ f являются ContMDiffAt в точке 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 contMDiffAt_prod_iff (f : M → M' × N') :
ContMDiffAt I (I'.prod J') n f x ↔ ContMDiffAt I I' n (Prod.fst ∘ f) x ∧ ContMDiffAt I J' n (Prod.snd ∘ f) x := by
simp_rw [← contMDiffWithinAt_univ]; exact contMDiffWithinAt_prod_iff f
