smul_const — Mathlib

English

If c is a differentiable-within-c set function and f is constant, then the derivative within s of y ↦ c(y) f equals derivWithin c s x times f.

Русский

Если c дифференцируема внутри s, а f константа, то внутри s производная y ↦ c(y) f равна derivWithin c s x, умноженной на f.

LaTeX

$$$\\operatorname{derivWithin}_s\\bigl(c(y)f\\bigr)(x) = \\operatorname{derivWithin}_s c(x)\\,f$$$

Lean4

theorem smul_const (hc : HasDerivWithinAt c c' s x) (f : F) : HasDerivWithinAt (fun y => c y • f) (c' • f) s x :=
  by
  have := hc.smul (hasDerivWithinAt_const x s f)
  rwa [smul_zero, zero_add] at this

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