mathlib

4a837fb9 - chore(analysis/normed/group): add a few convenience lemmas (#9770)

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`.