English
If c and f have FDerivWithinAt cad with respect to s, then the map y ↦ c(y)·f(y) has the FDerivWithinAt given by the product rule within s.
Русский
Если у c и f есть внутри множества s ФДериватив внутри s, то отображение y ↦ c(y)·f(y) имеет внутри s ФДериват внутри s по правилу произведения.
LaTeX
$$$$ \\text{HasFDerivWithinAt}(\\lambda y, c(y)·f(y), s, x) = c(x)·f' + c(x') smulRight (f(x)). $$$$
Lean4
@[fun_prop]
theorem fun_smul (hc : HasFDerivWithinAt c c' s x) (hf : HasFDerivWithinAt f f' s x) :
HasFDerivWithinAt (fun y => c y • f y) (c x • f' + c'.smulRight (f x)) s x := by
-- `by exact` to solve unification issues.
exact (isBoundedBilinearMap_smul.hasFDerivAt (𝕜 := 𝕜) (c x, f x)).comp_hasFDerivWithinAt x <| hc.prodMk hf
