fderiv_mul' — Mathlib

English

Let hxs, hc, hd hold; then fderivWithin 𝕜 (c * d) s x equals c(x) • fderivWithin d s x plus d(x) • fderivWithin c s x.

Русский

Пусть выполняются условия hxs, hc и hd; тогда fderivWithin 𝕜 (c d) s x равно c(x) • fderivWithin d s x плюс d(x) • fderivWithin c s x.

LaTeX

$$$\\forall hxs hc hd,\\ fderivWithin 𝕜 (c \\cdot d) s x = c(x) \\cdot fderivWithin 𝕜 d s x + d(x) \\cdot fderivWithin 𝕜 c s x$$$

Lean4

theorem fderiv_mul' (ha : DifferentiableAt 𝕜 a x) (hb : DifferentiableAt 𝕜 b x) :
    fderiv 𝕜 (a * b) x = a x • fderiv 𝕜 b x + fderiv 𝕜 a x <• b x :=
  (ha.hasFDerivAt.mul' hb.hasFDerivAt).fderiv

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