const_smul — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[fun_prop]
theorem const_smul (h : DifferentiableWithinAt 𝕜 f s x) (c : R) : DifferentiableWithinAt 𝕜 (c • f) s x :=
  h.fun_const_smul c

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