smul_const — Mathlib

English

If c is differentiable within s at x, then derivWithin (c(y) f) s x = derivWithin c s x · f, for fixed f.

Русский

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

LaTeX

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

Lean4

theorem smul_const (hc : HasDerivAt c c' x) (f : F) : HasDerivAt (fun y => c y • f) (c' • f) x :=
  by
  rw [← hasDerivWithinAt_univ] at *
  exact hc.smul_const f

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