Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-07-12 01:43 3d36966e

View on Github →

feat(analysis/calculus/mean_value): the mean value inequality (#1212)

feat(analysis/calculus/mean_value): the mean value inequality
remove blank lines

Estimated changes

Created src/analysis/calculus/mean_value.lean

added theorem norm_image_sub_le_of_norm_deriv_le_convex

added theorem norm_image_sub_le_of_norm_deriv_le_segment

Modified src/analysis/convex.lean

added theorem image_Icc_zero_one_eq_segment