theorem monotone_convergence_theorem {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal} {g : α → ENNReal} (hf_meas : ∀ (n : ℕ), Measurable (f n)) (hf_mono : Monotone f) (hf_lim : ∀ (x : α), Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (g x))) : Filter.Tendsto (fun (n : ℕ) => ∫⁻ (x : α), f n x ∂μ) Filter.atTop (nhds (∫⁻ (x : α), g x ∂μ))

Monotone convergence theorem (Lecture 5, "More integral properties"): if f_n : α → [0, ∞] is a pointwise non-decreasing sequence of measurable functions converging pointwise to g, then ∫ f_n dμ ↑ ∫ g dμ, i.e. the sequence of Lebesgue integrals tends to the integral of the limit.