Kőnig's lemma

Kőnig's lemma is the statement that a finitely branching tree is infinite if and only if it contains an infinite path.

Constructivity

While true in classical logic with the axiom of choice, Kőnig's lemma is not always true in constructive settings: see the Wikipedia link below.

Please expand.

References

• There is a Wikipedia page that explains more.