basic): add a few lemmas (#12259)

Commit

3 years ago

feat(topology/metric_space/basic): add a few lemmas (#12259) Add `ne_of_mem_sphere`, `subsingleton_closed_ball`, and `metric.subsingleton_sphere`.

Author

urkud

Parents