König's Lemma

This entire file is dedicated to proving König's Lemma on the FiniteDegreeTree. That is, we show that if every branch in a FiniteDegreeTree is finite, then there the set of FiniteDegreeTree.branches is finite. We show this result in branches_finite_of_each_branch_finite.

theorem FiniteDegreeTree.branches_finite_of_each_branch_finite {α : Type u_1} (t : FiniteDegreeTree α) : (∀ (b : PossiblyInfiniteList α), b ∈ t.branches → b.finite) → t.branches.finite

This is König's Lemma. If each branch is finite, then there are only finitely many branches. We show this essentially via contraposition, i.e. we assume that there are infinitely many branches and then we construct an infinite branch using generate_branch and the previously defined infinite_branch_generator.