sub — Mathlib

English

Let f,g: N → C and s ∈ C. If both f and g are L-series summable at s, then their difference f − g is also summable at s.

Русский

Пусть f,g : ℕ → ℂ и s ∈ ℂ. Если обе L-серии суммируемы в s для f и g, то и их разность f − g суммируема в s.

LaTeX

$$$\forall f,g:\mathbb{N}\to\mathbb{C},\ s\in\mathbb{C},\ LSeriesSummable\,f\,s \land LSeriesSummable\,g\,s \Rightarrow LSeriesSummable\,(f-g)\,s$$$

Lean4

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

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