Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-25 11:39 21435715

View on Github →

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

Estimated changes

added def Born.of
added def Born