mathlib3

f37f57dc - feat(order/lattice): `sup`/`inf`/`max`/`min` of mono functions (#9284)

feat(order/lattice): `sup`/`inf`/`max`/`min` of mono functions (#9284) * add `monotone.sup`, `monotone.inf`, `monotone.min`, and `monotone.max`; * add `prod.le_def` and `prod.mk_le_mk`.