Def Profinite.as_limit_cone_iso

Modification history

2021-05-07 22:54
src/topology/category/Profinite/as_limit.lean
feat(topology/category/*): Add alternative explicit limit cones for `Top`, etc. and shows `X : Profinite` is a limit of finite sets. (#7448) …
Added Profinite.as_limit_cone_isoView on Github →