fun_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,f',s,x) \\land \\text{HasDerivWithinAt}(g,g',s,x) \\Rightarrow \\text{HasDerivWithinAt}(f - g, f' - g', s, x)$$$

Lean4

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

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