Commit 2021-02-17 03:54 d4ef2e85

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.