English
If f and g have derivatives within s, then the pair (f,g) has derivative df.prod dg within s.
Русский
Если у f и g есть производные внутри s, то пара (f,g) имеет производную df.prod dg внутри s.
LaTeX
$$$ HasMFDerivWithinAt I I' f s x df \to HasMFDerivWithinAt I I'' g s x dg \to HasMFDerivWithinAt I (I' .prod I'') (fun y => (f y, g y)) s x (df.prod dg) $$$
Lean4
/-- If `f` and `g` have derivatives `df` and `dg` at `x`, respectively,
then `x ↦ (f x, g x)` has derivative `df.prod dg`. -/
theorem prodMk {f : M → M'} {g : M → M''} {df : TangentSpace I x →L[𝕜] TangentSpace I' (f x)}
(hf : HasMFDerivAt I I' f x df) {dg : TangentSpace I x →L[𝕜] TangentSpace I'' (g x)}
(hg : HasMFDerivAt I I'' g x dg) : HasMFDerivAt I (I'.prod I'') (fun y ↦ (f y, g y)) x (df.prod dg) :=
⟨hf.1.prodMk hg.1, hf.2.prodMk hg.2⟩
