Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-30 18:14 decd67c4

View on Github →

feat(analysis/convex): slope_mono_adjacent (#4307)

Estimated changes

Modified src/analysis/convex/basic.lean

added theorem concave_on.slope_mono_adjacent

added theorem concave_on_real_iff_slope_mono_adjacent

added theorem convex_on.slope_mono_adjacent

added theorem convex_on_real_iff_slope_mono_adjacent