Erdős problem 872
Each move claims exactly one pool element, so the minimax value never exceeds the number of already claimed elements plus the number of still unclaimed elements.
Sources
FormalConjectures/ErdosProblems/
872.lean
Retained formal statement
A trivial upper bound: a play can claim at most the elements of , so .
∀ (n : ℕ), 2 ≤ n → Erdos872.L n ≤ n - 1TextbookStatement only, no proof