Kőnig's infinity lemma

Kőnig's infinity lemma is most often stated as a graph theory result: every infinite, locally finite connected graph contains an infinite path. It has links to computability and proof theory, and it has a number of formulations.

In practice, most applications are not to an abstract graph, but to a concrete collection of objects that are organized in a graph-like way, often where the graph is a rooted tree representing a graded order. In fact, the lemma is most easily stated and proved in terms of covers in a strongly atomic order rather than a graph; in this setting, the proof is almost trivial.

A common formulation of Kőnig's lemma is in terms of directed systems, with the grading explicitly represented using an ℕ-indexed family of types, which we also provide in this module. This is a specialization of the much more general nonempty_sections_of_finite_cofiltered_system, which goes through topology and category theory, but here it is stated and proved independently with much fewer dependencies.

We leave the explicitly graph-theoretic version of the statement as TODO.

Main Results

• exists_seq_covby_of_forall_covby_finite : Kőnig's lemma for strongly atomic orders.

• exists_orderEmbedding_covby_of_forall_covby_finite : Kőnig's lemma, where the sequence is given as an OrderEmbedding instead of a function.

• exists_orderEmbedding_covby_of_forall_covby_finite_of_bot : Kőnig's lemma where the sequence starts at the minimum of an infinite type.

• exist_seq_forall_proj_of_forall_finite : Kőnig's lemma for inverse systems, proved using the above applied to an order on a sigma-type (i : ℕ) × α i.

TODO

Formulate the lemma as a statement about graphs.

theorem exists_seq_covby_of_forall_covby_finite {α : Type u_1} [PartialOrder α] [IsStronglyAtomic α] {b : α} (hfin : ∀ (a : α), {x : α | a ⋖ x}.Finite) (hb : (Set.Ici b).Infinite) : ∃ (f : ℕ → α), f 0 = b ∧ ∀ (i : ℕ), f i ⋖ f (i + 1)

Kőnig's infinity lemma : if each element in a strongly atomic order is covered by only finitely many others, and b is an element with infinitely many things above it, then there is a sequence starting with b in which each element is covered by the next.

theorem exists_orderEmbedding_covby_of_forall_covby_finite {α : Type u_1} [PartialOrder α] [IsStronglyAtomic α] {b : α} (hfin : ∀ (a : α), {x : α | a ⋖ x}.Finite) (hb : (Set.Ici b).Infinite) : ∃ (f : ℕ ↪o α), f 0 = b ∧ ∀ (i : ℕ), f i ⋖ f (i + 1)

The sequence given by Kőnig's lemma as an order embedding

theorem exists_orderEmbedding_covby_of_forall_covby_finite_of_bot {α : Type u_1} [PartialOrder α] [IsStronglyAtomic α] [OrderBot α] [Infinite α] (hfin : ∀ (a : α), {x : α | a ⋖ x}.Finite) : ∃ (f : ℕ ↪o α), f 0 = ⊥ ∧ ∀ (i : ℕ), f i ⋖ f (i + 1)

A version of Kőnig's lemma where the sequence starts at the minimum of an infinite order.

theorem GradeMinOrder.exists_nat_orderEmbedding_of_forall_covby_finite {α : Type u_1} [PartialOrder α] [IsStronglyAtomic α] [GradeMinOrder ℕ α] [OrderBot α] [Infinite α] (hfin : ∀ (a : α), {x : α | a ⋖ x}.Finite) : ∃ (f : ℕ ↪o α), f 0 = ⊥ ∧ (∀ (i : ℕ), f i ⋖ f (i + 1)) ∧ ∀ (i : ℕ), grade ℕ (f i) = i

theorem exists_seq_forall_proj_of_forall_finite {α : ℕ → Type u_1} [Finite (α 0)] [∀ (i : ℕ), Nonempty (α i)] (π : {i j : ℕ} → i ≤ j → α j → α i) (π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a) (π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a) (hfin : ∀ (i : ℕ) (a : α i), {b : α (i + 1) | π ⋯ b = a}.Finite) : ∃ (f : (i : ℕ) → α i), ∀ ⦃i j : ℕ⦄ (hij : i ≤ j), π hij (f j) = f i

A formulation of Kőnig's infinity lemma, useful in applications. Given a sequence α 0, α 1, ... of nonempty types with α 0 finite, and a well-behaved family of projections π : α j → α i for all i ≤ j, if each term in each α i is the projection of only finitely many terms in α (i+1), then we can find a sequence (f 0 : α 0), (f 1 : α 1), ... where f i is the projection of f j for all i ≤ j.

In a typical application, the α i are function types with increasingly large domains, and π hij (f : α j) is the restriction of the domain of f to that of α i. In this case, the sequence given by the lemma is essentially a function whose domain is the limit of the α i.

See also nonempty_sections_of_finite_cofiltered_system.