English
The inverse limit of a cofiltered diagram of nonempty finite sets is nonempty (Kőnig's lemma style).
Русский
Обратный предел диаграммы не пустых конечных множеств ко-фильтрованной диаграммы непуст.
LaTeX
$$$ \mathrm{Nonempty}(\mathrm{F}.\mathrm{sections}) $$$
Lean4
/-- The inverse limit of nonempty finite types is nonempty.
See `nonempty_sections_of_finite_cofiltered_system` for a generalization to cofiltered limits.
That version applies in almost all cases, and the only difference is that this version
allows `J` to be empty.
This may be regarded as a generalization of Kőnig's lemma.
To specialize: given a locally finite connected graph, take `Jᵒᵖ` to be `ℕ` and
`F j` to be length-`j` paths that start from an arbitrary fixed vertex.
Elements of `F.sections` can be read off as infinite rays in the graph. -/
theorem nonempty_sections_of_finite_inverse_system {J : Type u} [Preorder J] [IsDirected J (· ≤ ·)] (F : Jᵒᵖ ⥤ Type v)
[∀ j : Jᵒᵖ, Finite (F.obj j)] [∀ j : Jᵒᵖ, Nonempty (F.obj j)] : F.sections.Nonempty :=
nonempty_sections_of_finite_cofiltered_system F
