Theorems · Theorem · sequences and series

summable_sigma_of_nonneg

∀ {α : Type u_4} {β : α → Type u_3} {f : (x : α) × β x → ℝ},
  (∀ (x : (x : α) × β x), 0 ≤ f x) →
    (Summable f ↔ (∀ (x : α), Summable fun y => f ⟨x, y⟩) ∧ Summable fun x => ∑' (y : β x), f ⟨x, y⟩)

Defined in

Mathlib.Topology.Algebra.InfiniteSum.Real

Cited by

2 results in Mathlib

Foundations

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