Partition result about finite products of infinite trees
In mathematics, the Halpern–Läuchli theorem is a partition result about finite products of infinite trees. Its original purpose was to give a model for set theory in which the Boolean prime ideal theorem is true but the axiom of choice is false. It is often called the Halpern–Läuchli theorem, but the proper attribution for the theorem as it is formulated below is to Halpern–Läuchli–Laver–Pincus or HLLP (named after James D. Halpern, Hans Läuchli, Richard Laver, and David Pincus), following .
Let "d","r" ; ω, formula_1 be a sequence of finitely splitting trees of height ω. Let 
formula_2
then there exists a sequence of subtrees formula_3 strongly embedded in formula_1 such that
formula_5
Alternatively, let
 formula_6
and
 formula_7.
The HLLP theorem says that not only is the collection formula_8 partition regular for each "d"  ; "ω", but that the homogeneous subtree guaranteed by the theorem is strongly embedded in
formula_9