mathlib3

dad7ecf9 - feat(analysis/convex/quasiconvex): A quasilinear function is either monotone or antitone (#17801)

feat(analysis/convex/quasiconvex): A quasilinear function is either monotone or antitone (#17801) Fulfill a todo I left a year ago. The proof is a big case bash on the relative positions of the four variables. I minimised it as much as I could. The end result mentions convexity, but this is mostly order theory.