fderivWithin_mul_const — Mathlib

English

If hxs, and a is differentiable within s at x, then fderivWithin 𝕜 (fun y => c(y) * d) s x = d • fderivWithin 𝕜 c s x.

Русский

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

LaTeX

$$$\\forall hxs hc, d,\\ fderivWithin 𝕜 (y \\mapsto c(y) d) s x = d \\cdot fderivWithin 𝕜 c s x$$$

Lean4

theorem fderivWithin_mul_const (hxs : UniqueDiffWithinAt 𝕜 s x) (hc : DifferentiableWithinAt 𝕜 c s x) (d : 𝔸') :
    fderivWithin 𝕜 (fun y => c y * d) s x = d • fderivWithin 𝕜 c s x :=
  (hc.hasFDerivWithinAt.mul_const d).fderivWithin hxs

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