König's lemma

König's lemma or Kőnig's infinity lemma is a theorem in graph theory due to Dénes Kőnig (1927). It gives a sufficient condition for an infinite graph to have an infinitely long path. The computability aspects of this theorem have been thoroughly investigated by researchers in mathematical logic, especially in computability theory. This theorem also has important roles in constructive mathematics and proof theory.

Let G be a connected graph with infinitely many vertices that is locally finite (each vertex is adjacent to only finitely many other vertices). Then G contains a ray: a simple path (a path with no repeated vertices) that starts at one vertex and continues from it through infinitely many vertices.

A common special case of this is that every infinite tree contains either a vertex of infinite degree or an infinite simple path.

Let v_i be the set of vertices. As premise, we assume that this set is infinite and the graph is connected.

Start with any vertex v₁. Every one of the infinitely many vertices of G can be reached from v₁ with a simple path, and each such path must start with one of the finitely many vertices adjacent to v₁. There must be one of those adjacent vertices through which infinitely many vertices can be reached without going through v₁. If there were not, then the entire graph would be the union of finitely many finite sets, and thus finite, contradicting the assumption that the graph is infinite. We may thus pick one of these vertices and call it v₂.

Now infinitely many vertices of G can be reached from v₂ with a simple path which does not include the vertex v₁. Each such path must start with one of the finitely many vertices adjacent to v₂. So an argument similar to the one above shows that there must be one of those adjacent vertices through which infinitely many vertices can be reached; pick one and call it v₃.

...
Wikipedia