basic): Add `ball_comm` lemmas (#14858)

Commit

3 years ago

feat(topology/metric_space/basic): Add `ball_comm` lemmas (#14858) This adds `closed_ball` and `sphere` comm lemmas to go with the existing `mem_ball_comm`.

Author

linesthatinterlace

Parents

2b5a5770

mathlib3 ee123628 - feat(topology/metric_space/basic): Add `ball_comm` lemmas (#14858)

mathlib3
ee123628 - feat(topology/metric_space/basic): Add `ball_comm` lemmas (#14858)