English
Let f: E → F and g: G → F be differentiable at x and y respectively. Then the map H: E × G → F × F defined by H(p) = (f(p1), g(p2)) is differentiable at (x, y), and its derivative is the pair of derivatives (Df(x), Dg(y)); equivalently, H′(x, y)(u, v) = (Df(x)u, Dg(y)v).
Русский
Пусть f: E → F и g: G → F дифференцируемы в точках x и y. Тогда отображение H: E × G → F × F, заданное H(p) = (f(p1), g(p2)), дифференцируемо в точке (x, y), а его производная представляет собой пару производных (Df(x), Dg(y)); то есть DH(x, y)(u, v) = (Df(x)u, Dg(y)v).
LaTeX
$$$\\text{If } f: E \\to F \\text{ and } g: G \\to F \\text{ are differentiable at } x\\in E \\text{ and } y\\in G, \\\\ H: E \\times G \\to F \\times F, \\quad H(u,v)=(f(u),g(v)) \\\\ \\text{is differentiable at } (x,y) \\text{ with derivative } DH(x,y)(h,k)=(Df(x)h, Dg(y)k).$$$
Lean4
@[simp, fun_prop]
protected theorem prodMap (hf : DifferentiableAt 𝕜 f p.1) (hf₂ : DifferentiableAt 𝕜 f₂ p.2) :
DifferentiableAt 𝕜 (fun p : E × G => (f p.1, f₂ p.2)) p :=
(hf.comp p differentiableAt_fst).prodMk (hf₂.comp p differentiableAt_snd)
