A subset $A_1 \times B_1 \times C_1$ of $A \times B \times C$ is monochromatic under a 2-colouring $f : A \to B \to C \to \operatorname{Fin} 2$ if $f$ is constant on $A_1 \times B_1 \times C_1$.

The set of countable ordinals, expressed using Mathlib's ω_ 1.

The set of ordinals strictly below any $\gamma < \omega_1$ is countable.

Initial segments of ω₁ (as sets of Omega1 elements) are countable. This is the subtype-order version of countable_Iio_of_lt_omega1.

Any countable subset of $\omega_1$ is bounded strictly below some element of $\omega_1$. This uses the key property that $\omega_1$ has uncountable cofinality (it is regular).

Prikry–Mills counterexample (key lemma):

There exists a 2-colouring $f$ of a set of cardinality $\aleph_1$ cubed such that no countable box $A_1 \times B_1 \times C_1$ is monochromatic.

This is the unpublished result of Prikry and Mills (1978). The proof proceeds by transfinite induction along $\omega_1$, which has uncountable cofinality, ensuring every countable box is non-monochromatic.

Erdős Problem 1128 (disproved by Prikry–Mills, 1978):

Erdős asked whether every 2-colouring of $A \times B \times C$, where $|A| = |B| = |C| = \aleph_1$, must contain a monochromatic countable box $A_1 \times B_1 \times C_1$ with $|A_1| = |B_1| = |C_1| = \aleph_0$.

The answer is No: Prikry and Mills constructed a 2-colouring of $\omega_1^3$ with no monochromatic countable box.

Note: The positive statement asserts that every 2-colouring of every $\aleph_1^3$ contains a monochromatic countably infinite box. Since the answer is False, this positive statement fails.

Explicit form of Prikry–Mills:

There exists a 2-colouring of $\omega_1 \times \omega_1 \times \omega_1$ such that for every countably infinite $A_1, B_1, C_1 \subseteq \omega_1$, the box $A_1 \times B_1 \times C_1$ is not monochromatic.

This is the content of the Prikry–Mills theorem (1978, unpublished), stated using Lean's ordinal type {o : Ordinal // o < ω_ 1} as the representation of $\omega_1$.