mathlib3

bfa24650 - refactor(topology/metric_space/lipschitz): redefine for an `emetric_space` (#2035)

refactor(topology/metric_space/lipschitz): redefine for an `emetric_space` (#2035) * refactor(topology/metric_space/lipschitz): redefine for an `emetric_space` * Fix compile * Fixes, thanks @sgouzel Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>