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