mul_const — Mathlib

English

If a,b are differentiable at x, then fderiv of a*b at x equals a(x) • fderiv b x plus fderiv a x <• b x.

Русский

Если a,b дифференцируемы в точке x, то производная fderiv произведения a*b в точке x равна a(x) • fderiv b x плюс fderiv a x <• b x.

LaTeX

$$$\\forall hc, hd,\\ fderiv 𝕜 (a \\cdot b) x = a(x) \\cdot fderiv 𝕜 b x + fderiv 𝕜 a x \\cdot<\\!\\!\\!> b(x)$$$

Lean4

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

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