Commit 2021-04-07 19:05 68bd3253

View on Github →

feat(topology/category/Profinite): Profinite_to_Top creates limits. (#7070) This PR adds a proof that Profinite has limits by showing that the forgetful functor to Top creates limits.

Estimated changes

Modified src/topology/category/CompHaus.lean

modified def CompHaus_to_Top

Modified src/topology/category/Profinite.lean