fun_add — Mathlib

English

If f and g have derivatives f' and g' at x with respect to L, then f + g has derivative f' + g' at x with respect to L.

Русский

Если у функций f и g есть производные f' и g' в точке x относительно фильтра L, то сумма f+g имеет производную f'+g' в точке x относительно L.

LaTeX

$$$\forall (hf : \ HasDerivAtFilter\ f\ f'\ x\ L) (hg : \ HasDerivAtFilter\ g\ g'\ x\ L),\ HasDerivAtFilter (f + g) (f' + g') x L$$$

Lean4

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

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