Theorems · Theorem · sequences and series

summable_partition

∀ {α : Type u_3} {β : Type u_4} {f : β → ℝ},
  0 ≤ f →
    ∀ {s : α → Set β},
      (∀ (i : β), ∃! j, i ∈ s j) →
        (Summable f ↔ (∀ (j : α), Summable fun i => f ↑i) ∧ Summable fun j => ∑' (i : ↑(s j)), f ↑i)

Defined in

Mathlib.Topology.Algebra.InfiniteSum.Real

Cited by

1 results in Mathlib

Foundations

Depth 160 from the axioms · uses propext, Classical.choice, Quot.sound