Commit 2023-03-18 15:20 d01ce5bd

View on Github →

feat: port Topology.Category.Born (#2973)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/ConcreteCategory/Bundled.lean

Created Mathlib/Topology/Category/Born.lean

added def Born.of

added def Born