Commit 2023-09-06 23:43 2c0daa9c

View on Github →

feat: Category of Alexandrov-discrete spaces (#6986) Define AlexDisc, the category of Alexandrov-discrete topological spaces with continuous maps.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Order/Category/AlexDisc.lean

added def AlexDisc.Iso.mk

added theorem AlexDisc.coe_forgetToTop

added theorem AlexDisc.coe_of

added theorem AlexDisc.forgetToTop_of

added def AlexDisc.of

added def AlexDisc