fun_mul — Mathlib

English

If ha: HasStrictFDerivAt a a' x and hb: HasStrictFDerivAt b b' x, then HasStrictFDerivAt (y ↦ a(y) * b(y)) with derivative a x • b' + a' • b x.

Русский

Если ha: HasStrictFDerivAt a a' x и hb: HasStrictFDerivAt b b' x, тогда HasStrictFDerivAt (y ↦ a(y) * b(y)) имеет производную a x • b' + a' • b x.

LaTeX

$$$\text{HasStrictFDerivAt}\ a\ a'\ x \rightarrow \text{HasStrictFDerivAt}\ b\ b'\ x \rightarrow \text{HasStrictFDerivAt}\ (a(y) \cdot b(y))\ (a x \cdot b' + a' \cdot b x)\ x$$$

Lean4

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

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