hom): Locally bounded maps (#12046)

Commit

3 years ago

feat(topology/bornology/hom): Locally bounded maps (#12046) Define `locally_bounded_map`, the type of locally bounded maps between two bornologies.

Author

YaelDillies

Parents