English
A variant of the derivative-within-smul identity when the scalar field elements are used; the derivative distributes over smul by field elements.
Русский
Вариант формулы внутри множества, когда скалярное умножение осуществляется элементами поля; производная распределяется по умножению на поле.
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
/-- A variant of `derivWithin_const_smul` without differentiability assumption when the scalar
multiplication is by field elements. -/
theorem derivWithin_const_smul' {f : 𝕜 → F} {x : 𝕜} {R : Type*} [Field R] [Module R F] [SMulCommClass 𝕜 R F]
[ContinuousConstSMul R F] (c : R) : derivWithin (c • f) s x = c • derivWithin f s x :=
derivWithin_fun_const_smul' c
