fun_sub — Mathlib

English

If f and g have derivatives f' and g' at x along L, then the difference f − g has derivative f' − g' at x along L.

Русский

Если у f и g по сравнению с x вдоль L существуют производные f' и g', то производная от f − g равна f' − g'.

LaTeX

$$$ \\text{HasDerivAtFilter}(f - g)\,(f' - g')\ x\ L \\text{ given } \\text{HasDerivAtFilter}(f,f',x,L) \\land \\text{HasDerivAtFilter}(g,g',x,L)$$$

Lean4

theorem fun_sub (hf : HasDerivAtFilter f f' x L) (hg : HasDerivAtFilter g g' x L) :
    HasDerivAtFilter (fun x ↦ f x - g x) (f' - g') x L := by simpa only [sub_eq_add_neg] using hf.add hg.neg

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