Erdős-Rado theorem for pairs (source code)

= Erdős-Rado theorem for pairs
{c}
{title2=$(2^\lambda)^+\longrightarrow(\lambda^+)^2_\lambda$}

For every infinite <cardinal> $\lambda$, every coloring of pairs from $(2^\lambda)^+$ by $\lambda$ colors has a <monochromatic> subset of size $\lambda^+$. Construct an end-homogeneous tree by routing a new vertex through the least preceding vertices that match its colors to all previously chosen ancestors. An ancestor's color to every later vertex on a branch is constant. A node at height $\alpha$ is determined by its color sequence of length $\alpha$, so levels below $\lambda^+$ have size at most $\lambda^{|\alpha|}\leq2^\lambda$. The whole tree has more than $2^\lambda$ vertices, forcing a branch of length $\lambda^+$. One of the $\lambda$ ancestor-colors occurs $\lambda^+$ times, giving the required set.