neg — Mathlib

English

If f has a derivative at x in the sense of a filter L, then the derivative of −f at x with respect to the same filter is −f'.

Русский

Если у f существует производная в точке x по фильтру L, то для −f та же производная равна −f'.

LaTeX

$$$$ HasFDerivAtFilter\ f\ f'\ x\ L \Rightarrow HasFDerivAtFilter\ (-f)\ (-f')\ x\ L. $$$$

Lean4

theorem neg (h : HasFDerivAtFilter f f' x L) : HasFDerivAtFilter (-f) (-f') x L :=
  (-1 : F →L[𝕜] F).hasFDerivAtFilter.comp x h tendsto_map

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