const_smul — Mathlib

English

The MF-derivative of a sum s·f + g equals s·mfderiv(f) + mfderiv(g).

Русский

MF-дериватив суммы s·f + g равен сумме: s·mfderiv(f) + mfderiv(g).

LaTeX

$$$mfderiv I 𝓘(𝕜,E')(s\cdot f) z = s\cdot mfderiv I 𝓘(𝕜,E') f z$ and similarly for the sum: equals $s\cdot mfderiv f z + mfderiv g z$.$$

Lean4

theorem const_smul (s : 𝕜) (hf : MDifferentiable I 𝓘(𝕜, E') f) : MDifferentiable I 𝓘(𝕜, E') (s • f) := fun x =>
  (hf x).const_smul s

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