mathlib3

9ac2aa29 - feat(topology/metric_space/lipschitz): add `lipschitz_with.min` and `lipschitz_with.max` (#9744)

feat(topology/metric_space/lipschitz): add `lipschitz_with.min` and `lipschitz_with.max` (#9744) Also change assumptions in some lemmas in `algebra.order.group` from `[add_comm_group α] [linear_order α] [covariant_class α α (+) (≤)]` to `[linear_ordered_add_comm_group α]`. These two sets of assumptions are equivalent but the latter is more readable.