Commit 2021-10-17 02:23 4a837fb9

chore(analysis/normed/group): add a few convenience lemmas (#9770) Add lipschitz_on_with.norm_sub_le_of_le, lipschitz_with.norm_sub_le, and lipschitz_with.norm_sub_le_of_le.