mathlib3

78034350 - refactor(topology/metric_space/lipschitz): generalize to pseudo_emetric_space (#6831)

refactor(topology/metric_space/lipschitz): generalize to pseudo_emetric_space (#6831) This is part of a series of PR to introduce `semi_normed_group` in mathlib. We introduce here Lipschitz maps for `pseudo_emetric_space` (I also improve some theorem name in `topology/metric_space/emetric_space`).