basic): some lemmas about dist (#13343)

Commit

3 years ago

feat(topology/metric_space/basic): some lemmas about dist (#13343) from the sphere eversion project

Author

fpvandoorn

Parents