English
Let f: M → F₁ × F₂. Then ContMDiffAt I (modelWithCornersSelf 𝕜 (F₁ × F₂)) n f x iff ContMDiffAt I (modelWithCornersSelf 𝕜 F₁) n (Prod.fst ∘ f) x ∧ ContMDiffAt I (modelWithCornersSelf 𝕜 F₂) n (Prod.snd ∘ f) x.
Русский
Пусть f: M → F₁ × F₂. Тогда ContMDiffAt I (modelWithCornersSelf 𝕜 (F₁ × F₂)) n f x эквивалентно двум условиям: ContMDiffAt для fst ∘ f и snd ∘ f.
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 contMDiffOn_prod_iff (f : M → M' × N') :
ContMDiffOn I (I'.prod J') n f s ↔ ContMDiffOn I I' n (Prod.fst ∘ f) s ∧ ContMDiffOn I J' n (Prod.snd ∘ f) s :=
⟨fun h ↦
⟨fun x hx ↦ ((contMDiffWithinAt_prod_iff f).1 (h x hx)).1, fun x hx ↦
((contMDiffWithinAt_prod_iff f).1 (h x hx)).2⟩,
fun h x hx ↦ (contMDiffWithinAt_prod_iff f).2 ⟨h.1 x hx, h.2 x hx⟩⟩
