Mathlib v3 is deprecated. Go to Mathlib v4

Def Profinite.as_limit

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_limitView on Github →