König's lemma

König's lemma is a theorem in graph theory. It states that

if G is a connected graph with infinitely many vertices such that every vertex has finite degree (= number of immediately adjacent vertices), then every vertex of G is part of an infinitely long simple path.

A common special case of this is that every tree that contains infinitely many vertices, each having finite degree, has at least one infinite simple path.

Note that the vertex degrees have to be finite, but not bounded: it is possible to have one vertex of degree 10, another of degree 100, a third of degree 1000 etc.

The proof proceeds as follows. Start with the given 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₁. So there must be one of those adjacent vertices through which infinitely many vertices can be reached; pick one and call it v₂. Now, infinitely many vertices of G can be reached from v₂ with a simple path which doesn't use the vertex v₁. Each such path must start with one of the finitely many vertices adjacent to v₂. So there must be one of those adjacent vertices through which infinitely many vertices can be reached; pick one and call it v₃. Continuing in this fashion, an infinite simple path can be constructed (by mathematical induction).

One should note that this proof is not constructive, since it involves a proof by contradiction to establish that there exists an adjacent vertex from which infinitely many other vertices can be reached. Indeed the theorem cannot be proven in a constructive way.

The Mizar project has completely formalized and automatically checked the proof of a version of König's lemma in the file TREES_2.