const_sub — Mathlib

English

For any c, if HasDerivAtFilter f f' x L holds, then HasDerivAtFilter (fun t => c − f t) (−f') x L holds as well.

Русский

Пусть для данной функции f и точки x в фильтре L верно, что HasDerivAtFilter f f' x L. Тогда верно также HasDerivAtFilter (λ t, c − f t) (−f') x L.

LaTeX

$$$$ HasDerivAtFilter (\lambda x, c - f x) (-f') x L $$$$

Lean4

theorem const_sub (c : F) (hf : HasDerivAtFilter f f' x L) : HasDerivAtFilter (fun x ↦ c - f x) (-f') x L := by
  simpa only [sub_eq_add_neg] using hf.neg.const_add c

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