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 branches is finite. We show this result in branches_finite_of_each_branch_finite.

theorem FiniteDegreeTree.branches_empty_of_root_none {α : Type u_1} {t : FiniteDegreeTree α} : t.root = none → t.branches = fun (b : PossiblyInfiniteList α) => b = PossiblyInfiniteList.empty

If the root of the tree is none, then the branches only consist of the (unique) empty branch.

theorem FiniteDegreeTree.branches_finite_of_root_none {α : Type u_1} {t : FiniteDegreeTree α} : t.root = none → t.branches.finite

By the above theorem, the set of branches is finite if the root is none.

theorem FiniteDegreeTree.branches_finite_of_each_child_branches_finite {α : Type u_1} (t : FiniteDegreeTree α) : (∀ (c : FiniteDegreeTreeWithRoot α), c ∈ t.childTrees → c.val.branches.finite) → t.branches.finite

The set of branches is finite, if the set of branches in each childTrees is finite. This is simply because there are only finitely many childTrees in a FiniteDegreeTree.

noncomputable def FiniteDegreeTree.infinite_branch_generator {α : Type u_1} (inf_branch_tree : { t : FiniteDegreeTreeWithRoot α // ¬t.val.branches.finite }) : { t : FiniteDegreeTreeWithRoot α // t ∈ inf_branch_tree.val.val.childTrees ∧ ¬t.val.branches.finite }

For König's Lemma below, we need to be able to generate an infinite branch. For this, we aim to leverage FiniteDegreeTree.generate_branch but we need to define an appropriate generator function. This is exactly what happens here. By this, we generate an infinite list of FiniteDegreeTreeWithRoot where each tree has infinitely many branches, based on knowing that the previous tree has infinitely many branches. This works since if a tree has infinitely many branches but only finitely many children, then there needs to exists a child tree that has infinitely many branches. The function is noncomputable since we need Classical.choose to pick a suitable child tree.

Equations

• FiniteDegreeTree.infinite_branch_generator inf_branch_tree = ⟨Classical.choose ⋯, ⋯⟩

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.