add — Mathlib

English

Same as above: the derivative of a sum under HasDerivAtFilter is the sum of derivatives.

Русский

То же самое: производная суммы равна сумме производных в рамках HasDerivAtFilter.

LaTeX

$$$\text{HasDerivAtFilter} (f+g) (f'+g') x L$ given $\text{HasDerivAtFilter} f f' x L$ and $\text{HasDerivAtFilter} g g' x L$$$

Lean4

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

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