mathlib3

e0f80e78 - feat(analysis/convex/quasiconvex): Quasiconvexity of functions (#9561)

feat(analysis/convex/quasiconvex): Quasiconvexity of functions (#9561) A function is quasiconvex iff all its sublevels are convex. This generalizes unimodality to non-ordered spaces. Co-authored-by: Johan Commelin <johan@commelin.net>