Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-15 19:56 f1f4c23f

View on Github →

feat(analysis/convex/basic): convex_on lemmas (#7933)

Estimated changes

Modified src/analysis/convex/basic.lean

modified theorem concave_on.le_on_segment'

added theorem concave_on.le_right_of_left_le'

added theorem concave_on.le_right_of_left_le

added theorem concave_on.left_le_of_le_right'

added theorem concave_on.left_le_of_le_right

added theorem convex_on.le_left_of_right_le'

added theorem convex_on.le_left_of_right_le

modified theorem convex_on.le_on_segment'

modified theorem convex_on.le_on_segment

added theorem convex_on.le_right_of_left_le'

added theorem convex_on.le_right_of_left_le