basic): an order-bounded set is metric-bounded (#8335)

Commit

4 years ago

feat(topology/metric_space/basic): an order-bounded set is metric-bounded (#8335)

Author

ADedecker

Parents