Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-03 19:30 d416ad69

View on Github →

feat(topology/category/Profinite): add category of profinite top. spaces (#5147)

Estimated changes

Modified src/topology/category/CompHaus.lean

added theorem CompHaus.coe_to_Top

modified def CompHaus_to_Top

Created src/topology/category/Profinite.lean

added theorem Profinite.coe_to_Top

added structure Profinite

added def Profinite_to_CompHaus

added theorem Profinite_to_CompHaus_to_Top

added def Profinite_to_Top