derivWithin_mul_const — Mathlib

English

If hc and hd are HasStrictDerivAt for c and d, then the product has a strict derivative given by the standard product rule expression.

Русский

Если у c и d есть строгая производная в x, то их произведение имеет строгую производную по правилу произведения.

LaTeX

$$$\operatorname{HasStrictDerivAt}(c \cdot d) x = c'(x) d(x) + c(x) d'(x)$$$

Lean4

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

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