fun_add — Mathlib

English

If f and g have derivatives within s, then f + g has derivative f' + g' within s.

Русский

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

LaTeX

$$$ HasFDerivWithinAt f f' s x \rightarrow HasFDerivWithinAt g g' s x \rightarrow HasFDerivWithinAt (f + g) (f' + g') s x$$$

Lean4

@[fun_prop]
nonrec theorem fun_add (hf : HasFDerivWithinAt f f' s x) (hg : HasFDerivWithinAt g g' s x) :
    HasFDerivWithinAt (fun y => f y + g y) (f' + g') s x :=
  hf.add hg

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