fun_const_smul — Mathlib

English

If f is differentiable at x, then for any scalar c, the function y ↦ c · f(y) is differentiable at x.

Русский

Если f дифференцируема в точке x, то для любого скаляра c функция y → c · f(y) дифференцируема в x.

LaTeX

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

Lean4

@[fun_prop]
theorem fun_const_smul (h : DifferentiableAt 𝕜 f x) (c : R) : DifferentiableAt 𝕜 (fun y => c • f y) x :=
  (h.hasFDerivAt.const_smul c).differentiableAt

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