Theorems · Definition · sequences and series

Summable

{α : Type u_1} →
  {β : Type u_2} →
    [AddCommMonoid α] →
      [TopologicalSpace α] → (β → α) → optParam (SummationFilter β) (SummationFilter.unconditional β) → Prop

Summable f means that f has some (infinite) sum with respect to L. Use tsum to get the value.

Defined in

Mathlib.Topology.Algebra.InfiniteSum.Defs

Cited by

778 results in Mathlib

Foundations

Depth 57 from the axioms, rests on 924 definitions · uses propext, Classical.choice, Quot.sound

Assumes

AddCommMonoidTopologicalSpace