theorem MonotoneConvergence.monotone_convergence_theorem' {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal} (hf : ∀ (n : ℕ), Measurable (f n)) (h_mono : Monotone f) {E : Set α} (_hE : MeasurableSet E) : (Measurable fun (x : α) => ⨆ (n : ℕ), f n x) ∧ ∫⁻ (x : α) in E, ⨆ (n : ℕ), f n x ∂μ = ⨆ (n : ℕ), ∫⁻ (x : α) in E, f n x ∂μ ∧ Filter.Tendsto (fun (n : ℕ) => ∫⁻ (x : α) in E, f n x ∂μ) Filter.atTop (nhds (∫⁻ (x : α) in E, ⨆ (n : ℕ), f n x ∂μ))

Monotone Convergence Theorem (Beppo Levi) restricted to a measurable set: for a pointwise nondecreasing sequence of measurable ℝ≥0∞-valued functions, the pointwise supremum is measurable, the integral of the supremum equals the supremum of the integrals over E, and the sequence of integrals converges to that value.