Commit 2025-11-17 07:49 c878df9f
View on Github →feat(Integral): remove some completeness assumptions and generallize setIntegral_mono (#31660)
Remove some completeness assumptions in Bochner.Basic.
Generalize MeasureTheory.setIntegral_mono. Instead of only stating it for real functions, state it for functions taking values in an order-closed partial order which is an ordered monoid and also an ordered module. This matches the assumptions of MeasureTheory.integral_mono and covers for instance (n -> Real) when Fintype n.