mathlib3
1a780f69 - chore(topology/metric_space): export `is_compact_closed_ball` (#10973)

Commit

4 years ago

chore(topology/metric_space): export `is_compact_closed_ball` (#10973)

Author

urkud

urkud

Parents

Loading