Def topToLocale

Modification history

2023-05-16 15:19
Mathlib/Topology/Category/Locale.lean
feat: port Topology.Category.Locale (#4011)
Added topToLocaleView on Github →