Commit 2023-04-11 12:30 85b0cd3c

View on Github →

feat: port Topology.Category.Top.Adjunctions (#3390)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Category/Top/Adjunctions.lean

added def TopCat.adj₁

added def TopCat.adj₂