Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-12 18:01 5a9fb92b

View on Github →

feat(topology/category/Locale): The category of locales (#12580) Define Locale, the category of locales, as the opposite of Frame.

Estimated changes

added def Top_op_to_Frame
added theorem Locale.coe_of
added def Locale.of
added def Locale
added def Top_to_Locale