English
If hf and hg are ContDiffAt 𝕜 n f x and ContDiffAt 𝕜 n g y, then Prod.map f g is ContDiffAt 𝕜 n at (x,y).
Русский
Если f и g дифференцируемы до порядка n в точках x и y соответственно, то отображение (f,g) = Prod.map f g является ContDiffAt 𝕜 n в точке (x,y).
LaTeX
$$$\\forall f,g,x,y,\\; (hf:\\mathrm{ContDiffAt}_{\\mathbb{k}}\\ n\\ f\\ x)\\to(hg: \\mathrm{ContDiffAt}_{\\mathbb{k}}\\ n\\ g\\ y)\\Rightarrow \\mathrm{ContDiffAt}_{\\mathbb{k}}\\ n\\ (\\mathrm{Prod.map}\\ f\\ g)\\ (x,y)$$$
Lean4
/-- The product map of two `C^n` functions within a set at a point is `C^n`
within the product set at the product point. -/
@[fun_prop]
theorem prodMap {f : E → F} {g : E' → F'} {x : E} {y : E'} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g y) :
ContDiffAt 𝕜 n (Prod.map f g) (x, y) := by
rw [ContDiffAt] at *
simpa only [univ_prod_univ] using hf.prodMap hg
