mathlib

9a11efbc - feat(metric_space): add lipschitz_on_with (#4151)

feat(metric_space): add lipschitz_on_with (#4151) The order of the explicit arguments in this definition is open for negotiation. From the sphere eversion project. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>