summable_iff — Mathlib

English

If f and g are asymptotically equivalent on cofiniteness, then f is summable iff g is summable.

Русский

Если f и g эквивалентны по бесконечно большим индексам (кофинитно), то суммируемость f и суммируемость g равны

LaTeX

$$$ \\operatorname{IsEquivalent}(f,g) \\Rightarrow (\\operatorname{Summable}(f) \\iff \\operatorname{Summable}(g)) $$$

Lean4

theorem summable_iff {ι E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : ι → E}
    {g : ι → E} (h : f ~[cofinite] g) : Summable f ↔ Summable g :=
  ⟨fun hf => summable_of_isEquivalent hf h.symm, fun hg => summable_of_isEquivalent hg h⟩

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