add — Mathlib

English

If HasFDerivWithinAt holds for f and g, then their sum has derivative f' + g' within s at x.

Русский

Если HasFDerivWithinAt верно для f и g, то их сумма имеет производную f' + g' внутри s в x.

LaTeX

$$$ HasFDerivWithinAt f f' s x \rightarrow HasFDerivWithinAt g g' s x \rightarrow HasFDerivWithinAt (f + g) (f' + g') s x$$$

Lean4

@[fun_prop]
nonrec theorem add (hf : HasFDerivWithinAt f f' s x) (hg : HasFDerivWithinAt g g' s x) :
    HasFDerivWithinAt (f + g) (f' + g') s x :=
  hf.add hg

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