Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-29 20:27 3681b5a4

View on Github →

split(analysis/convex/slope): split slope results off analysis.convex.function (#9444)

Estimated changes

Modified src/analysis/calculus/mean_value.lean

Modified src/analysis/convex/function.lean

deleted theorem concave_on.slope_mono_adjacent

deleted theorem concave_on_iff_slope_mono_adjacent

deleted theorem concave_on_of_slope_mono_adjacent

deleted theorem convex_on.slope_mono_adjacent

deleted theorem convex_on_iff_slope_mono_adjacent

deleted theorem convex_on_of_slope_mono_adjacent

Created src/analysis/convex/slope.lean

added theorem concave_on.slope_anti_adjacent

added theorem concave_on_iff_slope_anti_adjacent

added theorem concave_on_of_slope_anti_adjacent

added theorem convex_on.slope_mono_adjacent

added theorem convex_on_iff_slope_mono_adjacent

added theorem convex_on_of_slope_mono_adjacent