Theorem MeasureTheory.SimpleFunc.lintegral_mono_fun

Modification history

2024-09-03 09:13
Mathlib/MeasureTheory/Function/SimpleFunc.lean
feat(Order/Lattice): add Monotone.of_map_inf_le_left etc (#15508) …
Added MeasureTheory.SimpleFunc.lintegral_mono_funView on Github →