mathlib

d4ef2e85 - feat(topology/category/Top): nonempty inverse limit of compact Hausdorff spaces (#6271)

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. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>