English
Assume c and f are differentiable within a set s at x, with derivatives c'(x) and f'(x). Then the within-derivative of y ↦ c(y) f(y) at x is c(x) f'(x) + c'(x) f(x).
Русский
Пусть c и f дифференцируемы внутри множества s в точке x, с производными c'(x) и f'(x). Тогда внутри множества s производная y ↦ c(y) f(y) в x равна c(x) f'(x) + c'(x) f(x).
LaTeX
$$$\\operatorname{derivWithin}_s\\bigl(c(y)f(y)\\bigr)(x) = c(x)\\operatorname{derivWithin}_s f(x) + \\operatorname{derivWithin}_s c(x)\\,f(x)$$$
Lean4
theorem derivWithin_fun_smul (hc : DifferentiableWithinAt 𝕜 c s x) (hf : DifferentiableWithinAt 𝕜 f s x) :
derivWithin (fun y => c y • f y) s x = c x • derivWithin f s x + derivWithin c s x • f x :=
by
by_cases hsx : UniqueDiffWithinAt 𝕜 s x
· exact (hc.hasDerivWithinAt.smul hf.hasDerivWithinAt).derivWithin hsx
· simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]
