derivWithin_const_smul — Mathlib

English

If c is constant and f is differentiable at x with derivative f', then the derivative of y ↦ c(y) f(y) reduces to c f' + f c' when c is differentiable; in constant case, derivative is c f'.

Русский

Если константа и f дифференцируемы, то производная функции y ↦ c(y) f(y) сводится к c f'(x) при константной c; для константной c является просто c f'(x).

LaTeX

$$$\\dfrac{d}{dy}\\bigl(c(y)f(y)\\bigr)\\Big|_{x} = c\,f'(x)$$$

Lean4

theorem derivWithin_const_smul (c : R) (hf : DifferentiableWithinAt 𝕜 f s x) :
    derivWithin (c • f) s x = c • derivWithin f s x :=
  derivWithin_fun_const_smul c hf

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