English
For c in a ring R acting on F and a differentiable function f, the within-derivative of y ↦ c(y) f(y) equals c(x) derivWithin f s x + derivWithin c s x · f(x).
Русский
Для c из кольца R, действующего на F, и функции f, дифференцируемой внутри s, внутренняя производная y ↦ c(y) f(y) равна c(x) derivWithin f s x + derivWithin c s 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_const_smul (c : R) (hf : DifferentiableWithinAt 𝕜 f s x) :
derivWithin (fun y => c • f y) s x = c • derivWithin f s x :=
by
by_cases hsx : UniqueDiffWithinAt 𝕜 s x
· exact (hf.hasDerivWithinAt.const_smul c).derivWithin hsx
· simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]
