mathlib

dbcd4546 - feat(topology/category/*): Add alternative explicit limit cones for `Top`, etc. and shows `X : Profinite` is a limit of finite sets. (#7448)

feat(topology/category/*): Add alternative explicit limit cones for `Top`, etc. and shows `X : Profinite` is a limit of finite sets. (#7448) This PR redefines `Top.limit_cone`, and defines similar explicit limit cones for `CompHaus` and `Profinite`. Using the definition with the subspace topology makes the proofs that the limit is compact, t2 and/or totally disconnected much easier. This also expresses any `X : Profinite` as a limit of its discrete quotients, which are all finite. Co-authored-by: Adam Topaz <adamtopaz@users.noreply.github.com>