Theorem MeasureTheory.integral_tendsto_of_tendsto_of_antitone

Modification history

2024-02-22 16:20
Mathlib/MeasureTheory/Integral/Bochner.lean
feat: add versions of the monotone convergence theorem for the Bochner integral (#10793)
Added MeasureTheory.integral_tendsto_of_tendsto_of_antitoneView on Github →