Commit 2024-09-03 09:13 ce66aa03
View on Github →feat(Order/Lattice): add Monotone.of_map_inf_le_left etc (#15508)
- Add
Monotone.of_map_inf_le_left
etc. - Use
Monotone.of_left_le_map_sup
to reorganize the proof ofSimpleFunc.lintegral_mono
. - Add
gcongr
attrs.