const_smul — Mathlib

English

In the filtered setting, if f has derivative f' at x in filter L and c is constant from R with compatible smul, then (c • f) has derivative c • f'.

Русский

В фильтрованной обстановке, если f имеет производную f' в x по фильтру L, и константа c совместима со скалярным умножением, то c • f имеет производную c • f'.

LaTeX

$$$\\operatorname{DerivAtFilter}_{x,L}(c\\cdot f) = c\\cdot f'$$$

Lean4

nonrec theorem const_smul (c : R) (hf : HasDerivAtFilter f f' x L) : HasDerivAtFilter (c • f) (c • f') x L := by
  simpa using (hf.const_smul c).hasDerivAtFilter

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