smul_const — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[fun_prop]
theorem smul_const (hc : DifferentiableWithinAt 𝕜 c s x) (f : F) : DifferentiableWithinAt 𝕜 (fun y => c y • f) s x :=
  (hc.hasFDerivWithinAt.smul_const f).differentiableWithinAt

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