mul' — Mathlib

English

If ha: HasFDerivWithinAt c c' s x and hb: HasFDerivWithinAt d d' s x, then HasFDerivWithinAt (y ↦ c(y) · d(y)) with derivative c x • d' + d x • c'.

Русский

Если ha: HasFDerivWithinAt c c' s x и hb: HasFDerivWithinAt d d' s x, тогда HasFDerivWithinAt (y ↦ c(y) · d(y)) имеет производную c(x) · d' + d(x) · c'.

LaTeX

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

Lean4

@[fun_prop]
theorem mul' (ha : HasFDerivWithinAt a a' s x) (hb : HasFDerivWithinAt b b' s x) :
    HasFDerivWithinAt (a * b) (a x • b' + a' <• b x) s x :=
  ha.fun_mul' hb

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