Borel determinacy theorem (source code)

= Borel determinacy theorem
{c}
{wiki}

Every <infinite game of perfect information> on a set-sized move alphabet with a Borel payoff in its discrete product topology has a <winning strategy in an infinite game> for one player. A proof strengthens the induction hypothesis to existence of arbitrary-depth-preserving <game coverings> unravelling the payoff. The closed-set announcement construction starts the induction. For countable unions, successive coverings stabilize each finite level and their inverse limit makes every constituent payoff clopen; their union is open and can be unravelled once more.