Topological Kőnig's lemma #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A topological version of Kőnig's lemma is that the inverse limit of nonempty compact Hausdorff spaces is nonempty. (Note: this can be generalized further to inverse limits of nonempty compact T0 spaces, where all the maps are closed maps; see [Sto79] --- however there is an erratum for Theorem 4 that the element in the inverse limit can have cofinally many components that are not closed points.)

We give this in a more general form, which is that cofiltered limits of nonempty compact Hausdorff spaces are nonempty (nonempty_limit_cone_of_compact_t2_cofiltered_system).

This also applies to inverse limits, where {J : Type u} [preorder J] [is_directed J (≤)] and F : Jᵒᵖ ⥤ Top.

The theorem is specialized to nonempty finite types (which are compact Hausdorff with the discrete topology) in lemmas nonempty_sections_of_finite_cofiltered_system and nonempty_sections_of_finite_inverse_system in the file category_theory.cofiltered_system.

(See https://stacks.math.columbia.edu/tag/086J for the Set version.)