fderivWithin_const_smul — Mathlib

English

In the field case, any constant c yields fderivWithin (c · f) = c · fderivWithin f.

Русский

В случае поля, для любого константного c выполняется fderivWithin (c · f) = c · fderivWithin f.

LaTeX

$$$ fderivWithin 𝕜 (c \cdot f) \, s \, x = c \cdot fderivWithin 𝕜 f \, s \, x$ для любого c ∈ 𝕜 (или эквивалентно через invertible c).$$

Lean4

theorem fderivWithin_const_smul (hxs : UniqueDiffWithinAt 𝕜 s x) (h : DifferentiableWithinAt 𝕜 f s x) (c : R) :
    fderivWithin 𝕜 (c • f) s x = c • fderivWithin 𝕜 f s x :=
  fderivWithin_fun_const_smul hxs h c

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