sub — Mathlib

English

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

Русский

Если f и g имеют суммы L-series a и b при s, то f − g имеет сумму a − b при s.

LaTeX

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

Lean4

theorem sub {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_sub] using HasSum.sub hf hg

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