König's lemma or König's infinity lemma is a theorem in graph theory due to Dénes Kőnig (1936). 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.
Read more about König's Lemma: Statement of The Lemma, Computability Aspects, Relationship To Constructive Mathematics and Compactness, Relationship With The Axiom of Choice