Commit 2021-10-16 09:26 9ac2aa29

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.