# Topological Kőnig's lemma #

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_limitCone_of_compact_t2_cofiltered_system).

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

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 Mathlib.CategoryTheory.CofilteredSystem.

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

def TopCat.partialSections {J : Type u} (F : ) {G : } (H : ) :
Set ((j : J) → (F.obj j))

Partial sections of a cofiltered limit are sections when restricted to a finite subset of objects and morphisms of J.

Equations
• = {u : (j : J) → (F.obj j) | ∀ {f : }, f H(F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}
Instances For
theorem TopCat.partialSections.nonempty {J : Type u} (F : ) [h : ∀ (j : J), Nonempty (F.obj j)] {G : } (H : ) :
.Nonempty
theorem TopCat.partialSections.directed {J : Type u} (F : ) :
Directed Superset fun (G : ) => TopCat.partialSections F G.snd
theorem TopCat.partialSections.closed {J : Type u} (F : ) [∀ (j : J), T2Space (F.obj j)] {G : } (H : ) :
theorem TopCat.nonempty_limitCone_of_compact_t2_cofiltered_system {J : Type u} (F : ) [∀ (j : J), Nonempty (F.obj j)] [∀ (j : J), CompactSpace (F.obj j)] [∀ (j : J), T2Space (F.obj j)] :
Nonempty .pt

Cofiltered limits of nonempty compact Hausdorff spaces are nonempty topological spaces.