Monotone convergence for ℝ≥0∞-valued sums

tsum commutes with the supremum of a monotone sequence of ℝ≥0∞-valued functions.

Main results

• ENNReal.tsum_iSup_of_monotone: the exchange of tsum and a monotone iSup.

theorem ENNReal.tsum_iSup_of_monotone {α : Type u_1} {f : ℕ → α → ENNReal} (hf : ∀ (a : α), Monotone fun (n : ℕ) => f n a) : ∑' (a : α), ⨆ (n : ℕ), f n a = ⨆ (n : ℕ), ∑' (a : α), f n a

Monotone convergence for ℝ≥0∞-valued sums: tsum commutes with a monotone iSup.