add — Mathlib

English

If f and g have strict derivatives at x, then f + g has a strict derivative equal to f' + g' at x.

Русский

Если у f и g в точке x существуют строгие производные f' и g', то у f + g в точке x есть строгая производная f' + g'.

LaTeX

$$$HasStrictDerivAt f f' x \land HasStrictDerivAt g g' x \Rightarrow HasStrictDerivAt (f + g) (f' + g') x$$$

Lean4

nonrec theorem add (hf : HasStrictDerivAt f f' x) (hg : HasStrictDerivAt g g' x) :
    HasStrictDerivAt (f + g) (f' + g') x := by simpa using (hf.add hg).hasStrictDerivAt

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