prodMap — Mathlib

English

If f and g are MDifferentiableAt at x and y respectively, then Prod.map f g is MDifferentiableAt at (x,y).

Русский

Пусть f и g дифференцируемы в точках x и y, тогда Prod.map f g дифференцируемо в точке (x,y).

LaTeX

$$$\text{MDifferentiableAt } I I' f x \land \text{MDifferentiableAt } J J' g y \Rightarrow \text{MDifferentiableAt } (I.prod J) (I'.prod J') (\mathrm{Prod.map}\ f\ g) (x,y)$$$

Lean4

theorem prodMap (hf : MDifferentiableAt I I' f x) (hg : MDifferentiableAt J J' g y) :
    MDifferentiableAt (I.prod J) (I'.prod J') (Prod.map f g) (x, y) :=
  by
  rw [← mdifferentiableWithinAt_univ] at *
  convert hf.prodMap hg
  exact univ_prod_univ.symm

Похожие утверждения