Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-03 22:32 dad7ecf9

View on Github →

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.

Estimated changes