summable_iff_nat — Mathlib

English

Let E be a normed additive group with a real vector space structure, and f,g : Nat → E. If g is Summable and f ~[atTop] g, then f is Summable.

Русский

Пусть E — нормированная абелева группа с вещественным пространством. Пусть f,g : Nat → E. Если g суммируема и f эквивалентна g на бесконечности, то и f суммируема.

LaTeX

$$$ \\operatorname{Summable}(g) \\land f ~_{\\mathrm{atTop}} g \\Rightarrow \\operatorname{Summable}(f) $$$

Lean4

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

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