Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-17 03:54 d4ef2e85

View on Github →

feat(topology/category/Top): nonempty inverse limit of compact Hausdorff spaces (#6271) The limit of an inverse system of nonempty compact Hausdorff spaces is nonempty, and this can be seen as a generalization of Kőnig's lemma. A future PR will address the weaker generalization that the limit of an inverse system of nonempty finite types is nonempty. This result could be generalized more, to the inverse limit of nonempty compact T0 spaces where all the maps are closed, but I think it involves an essentially different method.

Estimated changes