# Documentation

Mathlib.Topology.Category.TopCat.Limits.Konig

# 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 [Stone1979] --- 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.

Instances For
theorem TopCat.partialSections.nonempty {J : Type u} (F : ) [h : ∀ (j : J), Nonempty ↑(F.obj j)] {G : } (H : ) :
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.