fderivWithin_const_mul — Mathlib

English

If a is differentiable within s, then fderivWithin of λy. c(y) d equals d scaled with fderivWithin a s x.

Русский

Если a дифференцируема внутри s, то fderivWithin от λy. c(y) d равна d • fderivWithin a s x.

LaTeX

$$$\\operatorname{fderivWithin}_{\\mathbb{K}}\\big(\\lambda y. c(y) \\cdot d, s, x\\big) = d \\cdot \\operatorname{fderivWithin}_{\\mathbb{K}}(c, s, x)$$$

Lean4

theorem fderivWithin_const_mul (hxs : UniqueDiffWithinAt 𝕜 s x) (ha : DifferentiableWithinAt 𝕜 a s x) (b : 𝔸) :
    fderivWithin 𝕜 (fun y => b * a y) s x = b • fderivWithin 𝕜 a s x :=
  (ha.hasFDerivWithinAt.const_mul b).fderivWithin hxs

Похожие утверждения