add — Mathlib

English

If HasDerivWithinAt f f' s x and HasDerivWithinAt g g' s x, then HasDerivWithinAt (f + g) (f' + g') s x.

Русский

Пусть в точке x на множестве s функции f и g имеют производные внутри s f' и g'. Тогда сумма f + g имеет производную внутри s равную f' + g'.

LaTeX

$$$HasDerivWithinAt f f' s x \land HasDerivWithinAt g g' s x \Rightarrow HasDerivWithinAt (f + g) (f' + g') s x$$$

Lean4

nonrec theorem add (hf : HasDerivWithinAt f f' s x) (hg : HasDerivWithinAt g g' s x) :
    HasDerivWithinAt (f + g) (f' + g') s x :=
  hf.add hg

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