fun_add — Mathlib

English

If f and g have derivatives at x along filter L, then f + g has derivative f' + g' at x along L.

Русский

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

LaTeX

$$$ HasFDerivAtFilter f f' x L \Rightarrow HasFDerivAtFilter g g' x L \Rightarrow HasFDerivAtFilter (f + g) (f' + g') x L$$$

Lean4

theorem fun_add (hf : HasFDerivAtFilter f f' x L) (hg : HasFDerivAtFilter g g' x L) :
    HasFDerivAtFilter (fun y => f y + g y) (f' + g') x L :=
  .of_isLittleO <|
    (hf.isLittleO.add hg.isLittleO).congr_left fun _ =>
      by
      simp only [map_sub, add_apply]
      abel

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