English
Let f: M → F₁ × F₂. Then ContMDiffAt I (modelWithCornersSelf 𝕜 (F₁ × F₂)) n f x is equivalent to ContMDiffAt I (modelWithCornersSelf 𝕜 F₁) n (Prod.fst ∘ f) x and ContMDiffAt I (modelWithCornersSelf 𝕜 F₂) n (Prod.snd ∘ f) x.
Русский
Пусть f: M → F₁ × F₂. Тогда ContMDiffAt I (modelWithCornersSelf 𝕜 (F₁ × F₂)) n f x эквивалентно ContMDiffAt I (modelWithCornersSelf 𝕜 F₁) n (Prod.fst ∘ f) x и ContMDiffAt I (modelWithCornersSelf 𝕜 F₂) n (Prod.snd ∘ f) x.
LaTeX
$$$\\displaystyle \\operatorname{ContMDiffAt} \\\\ I \\\\ (I'.prod J') \\\\ n \\\\ f \\\\ x \\iff \\operatorname{ContMDiffAt} \\\\ I \\\\ (I'.prod J') \\\\ n \\\\ (\\mathrm{Prod.fst} \\circ f) \\ \\\\ x \\land \\operatorname{ContMDiffAt} \\\\ I \\\\ (I'.prod J') \\\\ n \\\\ (\\mathrm{Prod.snd} \\circ f) \\\\ x$$
Lean4
theorem contMDiff_prod_assoc :
ContMDiff ((I.prod I').prod J) (I.prod (I'.prod J)) n fun x : (M × M') × N => (x.1.1, x.1.2, x.2) :=
contMDiff_fst.fst.prodMk <| contMDiff_fst.snd.prodMk contMDiff_snd
