Theorem MeasureTheory.integral_mono_measure

Modification history

2026-01-26 08:43
Mathlib/MeasureTheory/Integral/Bochner/Basic.lean
feat(MeasureTheory/Probability): Generalize some theorems by replacing OrderClosedTopology with ClosedIciTopology (#34432) …
Modified MeasureTheory.integral_mono_measureView on Github →
2025-04-23 07:13
Mathlib/MeasureTheory/Integral/Bochner/Basic.lean
feat: generalize order properties of the Bochner integral to real ordered Banach spaces (#24177) …
Modified MeasureTheory.integral_mono_measureView on Github →
2023-06-05 08:37
Mathlib/MeasureTheory/Integral/Bochner.lean
feat: port MeasureTheory.Integral.Bochner (#4590)
Added MeasureTheory.integral_mono_measureView on Github →