smul_const — Mathlib

English

If c is differentiable at x with derivative c', then y ↦ c(y) · f is differentiable at x with derivative c'.smulRight f.

Русский

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

LaTeX

$$$\HasFDerivAt\ c\ c'\ x \Rightarrow \HasFDerivAt\ (\\lambda y. c(y) \\cdot f)\ (c'.smulRight f)\ x$$$

Lean4

@[fun_prop]
theorem smul_const (hc : DifferentiableAt 𝕜 c x) (f : F) : DifferentiableAt 𝕜 (fun y => c y • f) x :=
  (hc.hasFDerivAt.smul_const f).differentiableAt

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