English
Variant: no smoothness assumption on c, derivative exists in the filter sense, then derivAtFilter of c f equals c f' in the appropriate sense.
Русский
Вариант без предположения о гладкости c, существование производной в фильтре, затем derivAtFilter от c f равна соответствующей форме c f'.
LaTeX
$$$\\operatorname{HasDerivAtFilter}_{x,L}(c\\cdot f) = c\\cdot f'$$$
Lean4
/-- A variant of `derivWithin_fun_const_smul` without differentiability assumption when the scalar
multiplication is by field elements. -/
theorem derivWithin_fun_const_smul' {f : 𝕜 → F} {x : 𝕜} {R : Type*} [Field R] [Module R F] [SMulCommClass 𝕜 R F]
[ContinuousConstSMul R F] (c : R) : derivWithin (fun y ↦ c • f y) s x = c • derivWithin f s x :=
by
by_cases hsx : UniqueDiffWithinAt 𝕜 s x
· simp [← fderivWithin_derivWithin, ← Pi.smul_def, fderivWithin_const_smul_field c hsx]
· simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]
