English
Let f: M → M' × N'. Then f is C^n on s at x with respect to the product-chart I′×J′ if and only if the two coordinate maps fst ∘ f and snd ∘ f are separately C^n on s at x with respect to I,I′ and I,J′ respectively.
Русский
Пусть f: M → M' × N'. Тогда f является C^n на s в точке x относительно произведённой карты I′×J′ тогда и только тогда, когда по отдельности отображения fst ∘ f и snd ∘ f являются C^n на s в точке x относительно I,I′ и I,J′ соответственно.
LaTeX
$$$\\displaystyle \operatorname{ContMDiffWithinAt} \;I\\; (I'.prod J')\\; n\\; f\\; s\\; x \\; \\Longleftrightarrow \\; \\big( \\operatorname{ContMDiffWithinAt} \\;I\\; I'\\; n\\; (\\mathrm{Prod.fst} \\circ f)\\; s\\; x \\big) \\wedge \\big( \\operatorname{ContMDiffWithinAt} \\;I\\; J'\\; n\\; (\\mathrm{Prod.snd} \\circ f)\\; s\\; x \\big)$$
Lean4
theorem contMDiffWithinAt_prod_iff (f : M → M' × N') :
ContMDiffWithinAt I (I'.prod J') n f s x ↔
ContMDiffWithinAt I I' n (Prod.fst ∘ f) s x ∧ ContMDiffWithinAt I J' n (Prod.snd ∘ f) s x :=
⟨fun h => ⟨h.fst, h.snd⟩, fun h => h.1.prodMk h.2⟩
