const_smul — Mathlib

English

If f is differentiable on s, then c · f is differentiable on s for any scalar c.

Русский

Если f дифференцируема на s, то c · f дифференцируема на s.

LaTeX

$$$ (h : \mathrm{DifferentiableOn}_{\mathbb{K}} f \, s) \Rightarrow \forall c\in R, \mathrm{DifferentiableOn}_{\mathbb{K}} (c \cdot f) \, s$$$

Lean4

@[fun_prop]
theorem const_smul (h : DifferentiableOn 𝕜 f s) (c : R) : DifferentiableOn 𝕜 (c • f) s := fun x hx =>
  (h x hx).const_smul c

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