const_smul — Mathlib

English

If f has MF-derivative f' at z, then the scaled function s·f has MF-derivative s·f' at z.

Русский

Если у f есть MF-дериватив в точке z равный f', то у s·f есть MF-дериватив в точке z равный s·f'.

LaTeX

$$$\forall z\, {\cal H},\; HasMFDerivAt I 𝓘(𝕜,E') f z f' \Rightarrow HasMFDerivAt I 𝓘(𝕜,E') (s \cdot f) z (s \cdot f').$$$

Lean4

theorem const_smul (hf : HasMFDerivAt I 𝓘(𝕜, E') f z f') (s : 𝕜) : HasMFDerivAt I 𝓘(𝕜, E') (s • f) z (s • f') :=
  ⟨hf.1.const_smul s, hf.2.const_smul s⟩

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