Commit 2022-07-06 02:26 93e97d1e

View on Github →

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.

Estimated changes

Modified src/analysis/convex/function.lean

deleted theorem concave_on.le_right_of_left_le'

deleted theorem concave_on.le_right_of_left_le

added theorem concave_on.left_le_of_le_right''

added theorem concave_on.right_le_of_le_left''

added theorem concave_on.right_le_of_le_left'

added theorem concave_on.right_le_of_le_left

added theorem convex_on.le_left_of_right_le''

added theorem convex_on.le_right_of_left_le''