English
If hxs: UniqueDiffWithinAt 𝕜 s x and hc: DifferentiableWithinAt 𝕜 c s x, then fderivWithin 𝕜 (λ y. c(y) · f) s x = (fderivWithin 𝕜 c s x).smulRight f.
Русский
Если существуют уникальные точки для разности внутри, и c дифференцируема внутри s в x, то производная по f внутри s равна smulRight применённой к производной c.
LaTeX
$$$\text{UniqueDiffWithinAt } 𝕜\ s\ x \Rightarrow \text{DifferentiableWithinAt } 𝕜 c s x \Rightarrow fderivWithin 𝕜 (\\lambda y. c(y) \\cdot f)\ s\ x = (fderivWithin 𝕜 c s x).smulRight f$$$
Lean4
theorem fderivWithin_smul_const (hxs : UniqueDiffWithinAt 𝕜 s x) (hc : DifferentiableWithinAt 𝕜 c s x) (f : F) :
fderivWithin 𝕜 (fun y => c y • f) s x = (fderivWithin 𝕜 c s x).smulRight f :=
(hc.hasFDerivWithinAt.smul_const f).fderivWithin hxs
