const_smul_mfderiv — Mathlib

English

If f is MF-differentiable at z, then s·f is MF-differentiable at z with derivative s·f'.

Русский

Если f MF-дифференцируема в z, то s·f дифференцируема и имеет производную s·f'.

LaTeX

$$$\forall z,\; MDifferentiableAt I 𝓘(𝕜,E') f z \Rightarrow MDifferentiableAt I 𝓘(𝕜,E') (s\cdot f) z.$$

Lean4

theorem const_smul_mfderiv (hf : MDifferentiableAt I 𝓘(𝕜, E') f z) (s : 𝕜) :
    (mfderiv I 𝓘(𝕜, E') (s • f) z : TangentSpace I z →L[𝕜] E') =
      (s • mfderiv I 𝓘(𝕜, E') f z : TangentSpace I z →L[𝕜] E') :=
  (hf.hasMFDerivAt.const_smul s).mfderiv

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