mul — Mathlib

English

If c and d have strict derivatives at x, then the product map y ↦ c(y) · d(y) has derivative given by c x · d' + d x · c'.

Русский

Если функции c и d имеют строгое производное в x, то произведение y ↦ c(y) · d(y) имеет производную c x · d' + d x · c'.

LaTeX

$$$\text{HasStrictFDerivAt}\ c\ c'\ x \rightarrow \text{HasStrictFDerivAt}\ d\ d'\ x \rightarrow \text{HasStrictFDerivAt}\ (c(y) \cdot d(y))\ (c x \cdot d' + d x \cdot c')\ x$$$

Lean4

@[fun_prop]
theorem mul (hc : HasStrictFDerivAt c c' x) (hd : HasStrictFDerivAt d d' x) :
    HasStrictFDerivAt (c * d) (c x • d' + d x • c') x :=
  by
  convert hc.mul' hd
  ext z
  apply mul_comm

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