English
For f: M → F₁ × F₂, ContMDiffAt I 𝓘(𝕜, F₁ × F₂) n f x is equivalent to the conjunction of ContMDiffAt for the two coordinate maps with respective projection.
Русский
Для отображения f: M → F₁ × F₂ условие ContMDiffAt I 𝓘(𝕜, F₁ × F₂) n f x эквивалентно сходствy ContMDiffAt для двух координат: fst ∘ f и snd ∘ f.
LaTeX
$$$\\displaystyle \\operatorname{ContMDiffAt} \\\\ I \\\\ 𝓘(\\mathbb{k}, F_1 \\times F_2) \\\\ n \\\\ f \\\\ x \\iff \\\\ (\\operatorname{ContMDiffAt} \\\\ I \\\\ 𝓘(\\mathbb{k}, F_1) \\\\ n \\\\ (\\mathrm{Prod.fst} \\circ f) \\\\ x) \\land (\\operatorname{ContMDiffAt} \\\\ I \\\\ 𝓘(\\mathbb{k}, F_2) \\\\ n \\\\ (\\mathrm{Prod.snd} \\circ f) \\\\ x)$$
Lean4
theorem contMDiffAt_prod_module_iff (f : M → F₁ × F₂) :
ContMDiffAt I 𝓘(𝕜, F₁ × F₂) n f x ↔
ContMDiffAt I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) x ∧ ContMDiffAt I 𝓘(𝕜, F₂) n (Prod.snd ∘ f) x :=
by
rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]
exact contMDiffAt_prod_iff f
