mathlib

e7ea02fd - feat(analysis/convex/basic): Levels of a monotone/antitone function (#9547)

feat(analysis/convex/basic): Levels of a monotone/antitone function (#9547) The set of points whose image under a monotone function is less than a fixed value is convex, when the space is linear.