fderivWithin_mul_const' — Mathlib

English

If hxs holds, and a is differentiable within s at x with derivative a', then fderivWithin of y ↦ a(y) b equals a' acting on b.

Русский

Если выполнено hxs и a дифференцируема внутри s в x с производной a', то fderivWithin (y ↦ a(y) b) равно a' действующая на b.

LaTeX

$$$\\forall hxs ha, b,\\ fderivWithin 𝕜 (y \\mapsto a(y) b) s x = a' <• b$$$

Lean4

theorem fderivWithin_mul_const' (hxs : UniqueDiffWithinAt 𝕜 s x) (ha : DifferentiableWithinAt 𝕜 a s x) (b : 𝔸) :
    fderivWithin 𝕜 (fun y => a y * b) s x = fderivWithin 𝕜 a s x <• b :=
  (ha.hasFDerivWithinAt.mul_const' b).fderivWithin hxs

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