mathlib

93e97d1e - feat(analysis/convex/function): Variants of `convex_on.le_right_of_left_le` (#14821)

feat(analysis/convex/function): Variants of `convex_on.le_right_of_left_le` (#14821) This PR adds four variants of `convex_on.le_right_of_left_le` that are useful when dealing with convex functions on the real numbers.