add — Mathlib

English

If f and g are L-series summable at s, then f+g is L-series summable at s.

Русский

Если f и g суммируемы по L-series в s, то f+g суммируем по L-series в s.

LaTeX

$$$$ \text{If } \mathrm{LSeriesSummable}(f,s) \text{ and } \mathrm{LSeriesSummable}(g,s), \; \mathrm{LSeriesSummable}(f+g,s). $$$$

Lean4

theorem add {f g : ℕ → ℂ} {s : ℂ} (hf : LSeriesSummable f s) (hg : LSeriesSummable g s) : LSeriesSummable (f + g) s :=
  by simpa [LSeriesSummable, ← term_add_apply] using Summable.add hf hg

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