basic): a continuous function is bounded on a neighborhood of a compact set (#17457)

Commit

3 years ago

feat(topology/metric_space/basic): a continuous function is bounded on a neighborhood of a compact set (#17457)

Author

sgouezel

Parents