sub — Mathlib

English

If f and g have derivatives f' and g' within s at x, then f − g has derivative f' − g' within s at x.

Русский

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

LaTeX

$$$ \\text{HasDerivWithinAt}(f - g, f' - g', s, x)$ given $ \\text{HasDerivWithinAt}(f,f',s,x) \\land \\text{HasDerivWithinAt}(g,g',s,x)$$$

Lean4

nonrec theorem sub (hf : HasDerivWithinAt f f' s x) (hg : HasDerivWithinAt g g' s x) :
    HasDerivWithinAt (f - g) (f' - g') s x :=
  hf.sub hg

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