Konigs_Tree_Lemma
Proved⚠️ Retired — incorrect formalization
The Lean statement below does not express the result
Konigs_Tree_Lemmais named for, so itsProvedstatus carries no information about it. Do not import it or use it as a dependency.
If a rooted tree has infinitely many nodes and each node has finitely many children, then the tree has an infinite branch.
Why this node was retired
The posted statement is
theorem Konigs_Tree_Lemma {α : Type _} (f : ℕ → Finset α) (hne : ∀ n, (f n).Nonempty) (hconn : ∀ n, ∀ x ∈ f (n + 1), ∃ y ∈ f n, True) : ∃ g : ℕ → α, ∀ n, g n ∈ f n := by sorry
The connectivity hypothesis is ∀ n, ∀ x ∈ f (n + 1), ∃ y ∈ f n, True, which says only that each f n is nonempty — it records no edge between x and y. With the tree structure gone, the conclusion ∃ g, ∀ n, g n ∈ f n follows from hne alone by choice, so the statement is a restatement of the axiom of choice rather than König's lemma.
What a faithful statement would require
The hypothesis must carry an actual parent relation (∃ y ∈ f n, R y x for a given adjacency R), and the conclusion must require the chosen branch to respect it: ∀ n, R (g n) (g (n + 1)).
No corrected replacement node exists yet.
import Mathlib.Analysis.Complex.Basic
theorem Konigs_Tree_Lemma {α : Type _} (f : ℕ → Finset α) (hne : ∀ n, (f n).Nonempty) (hconn : ∀ n, ∀ x ∈ f (n + 1), ∃ y ∈ f n, True) : ∃ g : ℕ → α, ∀ n, g n ∈ f n := by sorry