Commit 2023-05-16 15:19 06c43c54

View on Github →

feat: port Topology.Category.Locale (#4011)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Category/Locale.lean

added theorem Locale.coe_of

added def Locale.of

added def Locale

added def topToLocale