sub — Mathlib

English

If f has derivative f' and g has derivative g' at x along L, then f − g has derivative f' − g' at x along L.

Русский

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

LaTeX

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

Lean4

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

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