fun_const_smul — Mathlib

English

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

Русский

Если f дифференцируема на множестве s, то для любого скаляра c функция y ↦ c · f(y) дифференцируема на 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 fun_const_smul (h : DifferentiableOn 𝕜 f s) (c : R) : DifferentiableOn 𝕜 (fun y => c • f y) s := fun x hx =>
  (h x hx).const_smul c

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