Skip to content

Erdős problem 872

Start work

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

The source's own material, retained exactly.

6 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

872.lean

Retained formal statement5 of 6

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.

FormalConjectures/ErdosProblems/872.leanErdos872.gameValueAux_le2 linesExact file
∀ {n : ℕ} (fuel : ℕ) (turn : Bool) (p : Erdos872.GamePos n),  Erdos872.gameValueAux fuel turn p ≤ p.claimed.card + p.pool.card
APIStatement only, no proof