derivWithin_smul_const — Mathlib

English

If c and f have strict derivatives at x, then the product y ↦ c(y) f(y) has strict derivative at x equal to c(x) f' + c' f(x).

Русский

Если c и f имеют строгие производные в x, то произведение c(y) f(y) имеет строгую производную в x: c(x) f'(x) + c'(x) f(x).

LaTeX

$$$\\dfrac{d}{dy}\\bigl(c(y)f(y)\\bigr)\\Big|_{y=x} = c(x) f'(x) + c'(x) f(x)$$$

Lean4

theorem derivWithin_smul_const (hc : DifferentiableWithinAt 𝕜 c s x) (f : F) :
    derivWithin (fun y => c y • f) s x = derivWithin c s x • f :=
  by
  by_cases hsx : UniqueDiffWithinAt 𝕜 s x
  · exact (hc.hasDerivWithinAt.smul_const f).derivWithin hsx
  · simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]

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