Open Ramsey theorem (source code)

= Open Ramsey theorem
{c}

Every <open set> $O$ in the <ordinary topology on infinite subsets> is a <Ramsey set of infinite subsets>: some infinite $B$ has $[B]^\omega\subseteq O$ or $[B]^\omega\cap O=\varnothing$. Use <acceptance and rejection of finite stems> and fusion to decide every finite stem. If the empty stem is rejected, each rejected stem has only finitely many accepting one-point extensions. Successive avoidance of these finite obstructions gives an infinite set all of whose finite stems are rejected; openness then excludes every infinite subset from $O$. This concerns increasing enumerations of infinite subsets, rather than unrestricted sequences with repetitions.