Born): The category of bornologies (#12045)

Commit

3 years ago

feat(topology/category/Born): The category of bornologies (#12045) Define `Born`, the category of bornological spaces with bounded maps.

Author

YaelDillies

Parents