derivWithin_const_mul — Mathlib

English

If d is differentiable within s at x, then the derivative within s of the constant multiple c · d is c times the derivative within s of d.

Русский

Если d дифференцируема внутри множества s в точке x, то производная внутри s от константного множителя c · d равна c умножить на производную внутри s от d.

LaTeX

$$$ \mathrm{derivWithin}_s (c \cdot d)(x) = c \cdot \mathrm{derivWithin}_s(d)(x) $$$

Lean4

theorem derivWithin_const_mul (c : 𝔸) (hd : DifferentiableWithinAt 𝕜 d s x) :
    derivWithin (fun y => c * d y) s x = c * derivWithin d s x :=
  by
  by_cases hsx : UniqueDiffWithinAt 𝕜 s x
  · exact (hd.hasDerivWithinAt.const_mul c).derivWithin hsx
  · simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]

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