Theorems · Theorem · sequences and series

summable_prod_of_nonneg

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

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