add — Mathlib

English

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

Русский

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

LaTeX

$$$ HasStrictFDerivAt f f' x \ to HasStrictFDerivAt g g' x \Rightarrow HasStrictFDerivAt (f + g) (f' + g') x$$$

Lean4

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

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