lipschitz): add several lemmas (#15634)

Commit

3 years ago

feat(topology/metric_space/lipschitz): add several lemmas (#15634) Some of these lemmas come from the sphere eversion project, with slightly different names.

Author

urkud

Parents

a095eaeb

mathlib3 d43aef06 - feat(topology/metric_space/lipschitz): add several lemmas (#15634)

mathlib3
d43aef06 - feat(topology/metric_space/lipschitz): add several lemmas (#15634)