Open determinacy (source code)

= Open determinacy

An <infinite game of perfect information> with an <open set> of winning plays for I in the <product topology> on a discrete move set has a <winning strategy in an infinite game> for one player. Construct a <winning-position attractor in an infinite game> by <transfinite recursion>; ranks give I a terminating descent strategy inside it, and its complement gives II a strategy avoiding every winning prefix. The move set need not be countable, in the usual set theory with <axiom of choice>.