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 of SimpleFunc.lintegral_mono.
  • Add gcongr attrs.

Estimated changes