fderivWithin_fun_const_smul — Mathlib

English

If hxs is UniqueDiffWithinAt and f is differentiable within s at x, then fderivWithin of c · f equals c times fderivWithin f.

Русский

Если hxs = UniqueDiffWithinAt 𝕜 s x и f дифференцируема внутри s в x, то fderivWithin (c · f) = c · fderivWithin f на s в x.

LaTeX

$$$ fderivWithin 𝕜 (c \cdot f) \, s \, x = c \cdot fderivWithin 𝕜 f \, s \, x$ под условием уникальности точки.$$

Lean4

theorem fderivWithin_fun_const_smul (hxs : UniqueDiffWithinAt 𝕜 s x) (h : DifferentiableWithinAt 𝕜 f s x) (c : R) :
    fderivWithin 𝕜 (fun y => c • f y) s x = c • fderivWithin 𝕜 f s x :=
  (h.hasFDerivWithinAt.const_smul c).fderivWithin hxs

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