mathlib3
5a9fb92b - feat(topology/category/Locale): The category of locales (#12580)

Commit
3 years ago
feat(topology/category/Locale): The category of locales (#12580) Define `Locale`, the category of locales, as the opposite of `Frame`.
Author
Parents
Loading