const_mul — Mathlib

English

If a is differentiable within s at x, then y ↦ c(y) d is differentiable within s at x.

Русский

Если a дифференцируема внутри s в точке x, то y ↦ c(y) d дифференцируема внутри s в x.

LaTeX

$$$\\text{DifferentiableWithinAt }\\mathbb{K}\\, a\\, s\\, x \\Rightarrow \\text{DifferentiableWithinAt }\\mathbb{K}\\, (\\lambda y. c(y) \\cdot d)\\, s\\, x$$$

Lean4

@[fun_prop]
theorem const_mul (ha : DifferentiableWithinAt 𝕜 a s x) (b : 𝔸) : DifferentiableWithinAt 𝕜 (fun y => b * a y) s x :=
  (ha.hasFDerivWithinAt.const_mul b).differentiableWithinAt

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