|
|
There is also a theorem of set theory called König's theorem.
König's lemma or König's infinity lemma is a theorem in graph theory due to Denes König that states
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 v1. Every one of the infinitely many vertices of G can be reached from v1 with a simple path, and each such path must start with one of the finitely many vertices adjacent to v1. So there must be one of those adjacent vertices through which infinitely many vertices can be reached; pick one and call it v2. Now, infinitely many vertices of G can be reached from v2 with a simple path which doesn't use the vertex v1. Each such path must start with one of the finitely many vertices adjacent to v2. So there must be one of those adjacent vertices through which infinitely many vertices can be reached; pick one and call it v3. 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 (http://mizar.org/JFM/Vol3/trees_2.html).