summable_of_isEquivalent — Mathlib

English

Let f,g : ι → E with E a normed additive group, and suppose g is summable and f is cofinite-equivalent to g. Then f is summable.

Русский

Пусть f,g : ι → E, где E — нормированная абелева группа. Если g суммируема и f эквивалентна g по кадрам дофинитного множества, то и f суммируема.

LaTeX

$$$ \\operatorname{Summable}(g) \\land f \\sim_{\\text{cofinite}} g \\Rightarrow \\operatorname{Summable}(f) $$$

Lean4

theorem summable_of_isEquivalent {ι E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    {f : ι → E} {g : ι → E} (hg : Summable g) (h : f ~[cofinite] g) : Summable f :=
  hg.trans_sub (summable_of_isBigO' hg h.isLittleO.isBigO)

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