fun_add — Mathlib

English

Let f and g have strict derivatives f' and g' at x. Then f + g has strict derivative f' + g' at x.

Русский

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

LaTeX

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

Lean4

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

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