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 (HLLP), following (Milliken 1979).
Let d,r < ω, be a sequence of finitely splitting trees of height ω. Let :