add — Mathlib

English

If f and g have L-series sums at s with values a and b, then f+g has L-series sum a+b at s.

Русский

Если у f и g есть суммы L-series в точке s со значениями a и b, то у f+g сумма равна a+b в точке s.

LaTeX

$$$$ \mathrm{LSeriesHasSum}(f+g)\, s\, (a+b) \;\text{from}\; \mathrm{LSeriesHasSum}(f)\, s\, a \; \text{и}\; \mathrm{LSeriesHasSum}(g)\, s\, b. $$$$

Lean4

theorem add {f g : ℕ → ℂ} {s a b : ℂ} (hf : LSeriesHasSum f s a) (hg : LSeriesHasSum g s b) :
    LSeriesHasSum (f + g) s (a + b) := by simpa [LSeriesHasSum, term_add] using HasSum.add hf hg

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