norm_image_sub_le_of_norm_deriv_le_segment

The mean value theorem along a segment: a bound on the derivative of a function along a segment implies a bound on the distance of the endpoints images

norm_image_sub_le_of_norm_deriv_le_convex

The mean value theorem on a convex set: if the derivative of a function is bounded by C, then the function is C-Lipschitz