Existing in Mathlib · Measure theory and analysis
Monotone Convergence Theorem
If measurable nonnegative functions grow pointwise with the sequence index, then integrating their pointwise supremum gives the same extended value as taking the supremum of their integrals.
- monotone convergence
- Lebesgue integration
- nonnegative extended reals
- pointwise suprema
- measurable functions
- lintegrals
Exact theorem
Exact Mathlib statement
theorem MeasureTheory.lintegral_iSup {α : Type*} {m : MeasurableSpace α} {μ : Measure α} {f : ℕ → α → ℝ≥0∞} (hf : ∀ n, Measurable (f n)) (h_mono : Monotone f) : ∫⁻ a, ⨆ n, f n a ∂μ = ⨆ n, ∫⁻ a, f n a ∂μThe theorem at a glance
Monotone Convergence Theorem at a glance
A visual guide to the theorem's hypotheses, structure, and conclusion; the exact statement gives the formal detail.
Monotone Convergence Theorem at a glance
Detailed visual description
The poster sets four nested green profiles above growing cobalt mass basins and centers the exact nonnegative extended-real lintegral equality. Its footer states the natural-number sequence, absence of integrability or finiteness hypotheses, and possible infinite common value.
Statement structure
From hypotheses to conclusion
This map summarizes the statement's structure; the exact Mathlib declaration remains authoritative.
Monotone Convergence Theorem — scientific diagram
Detailed visual description
This page indexes Mathlib's monotone convergence theorem for a natural-number-indexed sequence f : ℕ → α → ℝ≥0∞ whose terms are measurable and which is monotone in the pointwise function order. It concludes that the lintegral of the pointwise supremum equals the supremum of the lintegrals. Nonnegativity is encoded by ℝ≥0∞, so no integrability or finiteness hypothesis is required and either side may be ∞. The selected declaration does not state the nearby almost-everywhere-measurable/almost-everywhere-monotone variant, a signed or Bochner-integral theorem, convergence for a nonmonotone sequence, or a quantitative rate.
Why it matters
A mathematical landmark
The monotone convergence theorem is a foundational limit-interchange principle in measure theory. It allows nonnegative mass to be assembled through an increasing sequence without an integrable dominating function and underlies the construction and structural properties of the Lebesgue integral.
ProofAtlas record
What has been checked
Mathlib is the source of the theorem; the local Lean replay and page review are separate.
Claim boundary
No new theorem is claimed
This page indexes Mathlib's monotone convergence theorem for a natural-number-indexed sequence f : ℕ → α → ℝ≥0∞ whose terms are measurable and which is monotone in the pointwise function order. It concludes that the lintegral of the pointwise supremum equals the supremum of the lintegrals. Nonnegativity is encoded by ℝ≥0∞, so no integrability or finiteness hypothesis is required and either side may be ∞. The selected declaration does not state the nearby almost-everywhere-measurable/almost-everywhere-monotone variant, a signed or Bochner-integral theorem, convergence for a nonmonotone sequence, or a quantitative rate.
- Proof Atlas did not originate the monotone convergence theorem or Mathlib's declaration.
- The selected declaration requires ordinary measurability of every term and pointwise monotonicity in the function order, not merely almost-everywhere versions.
- The conclusion concerns ℝ≥0∞-valued lintegrals and permits the common value ∞; it is not a signed or Bochner-integral statement.
- The generated explanation and visuals are not proof evidence.
Source and local evidence
Where the theorem comes from
- Existing declaration
MeasureTheory.lintegral_iSupin mathlib- Relationship
- The checked artifact is the upstream declaration itself
- Local Lean evidence
artifact.library.mathlib.monotone-convergence-theorem.v001