mathlib

68bd3253 - feat(topology/category/Profinite): Profinite_to_Top creates limits. (#7070)

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.