English
Let f: M → F₁ × F₂. Then f is ContMDiffWithinAt I 𝓘(𝕜,F₁×F₂) n f s x if and only if the two projections are ContMDiffWithinAt with the corresponding charts, i.e., Prod.fst ∘ f and Prod.snd ∘ f are each ContMDiffWithinAt with respect to I and the models for F₁ and F₂.
Русский
Пусть f: M → F₁ × F₂. Тогда f ∈ ContMDiffWithinAt I 𝓘(𝕜,F₁×F₂) n на f относительно s в x тогда и только тогда, когда обе проекции fst ∘ f и snd ∘ f гладки в соответствующих схемах.
LaTeX
$$$\\displaystyle \\operatorname{ContMDiffWithinAt} \\\\ I \\\\ 𝓘(\\mathbb{k}, F_1 \\times F_2) \\\\ n \\\\ f \\\\ s \\\\ x \\iff \\\\ (\\operatorname{ContMDiffWithinAt} \\\\ I \\\\ 𝓘(\\mathbb{k}, F_1) \\\\ n \\\\ (\\mathrm{Prod.fst} \\circ f) \\\\ s \\\\ x) \\land (\\operatorname{ContMDiffWithinAt} \\\\ I \\\\ 𝓘(\\mathbb{k}, F_2) \\\\ n \\\\ (\\mathrm{Prod.snd} \\circ f) \\\\ s \\\\ x)$$
Lean4
theorem contMDiffWithinAt_prod_module_iff (f : M → F₁ × F₂) :
ContMDiffWithinAt I 𝓘(𝕜, F₁ × F₂) n f s x ↔
ContMDiffWithinAt I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) s x ∧ ContMDiffWithinAt I 𝓘(𝕜, F₂) n (Prod.snd ∘ f) s x :=
by
rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]
exact contMDiffWithinAt_prod_iff f
