Finite-support products

Let $I$ be a set and $(P_i,{\le }_i,1_i{)}_{i\in I}$ a family of posets with specified greatest elements. Put

${\prod }_{i\in I}^{\mathrm{f}\mathrm{i}\mathrm{n}}{P}_i=\{p\in {\prod }_{i\in I}{P}_i:\mathrm{supp}(p)=\{i\in I:p(i)\mathrm{\ne }{1}_i\}\text{ is finite}\}\mathrm{.}$

Order these tuples coordinatewise: $p\le q$ iff $p(i){\le }_{i}q(i)$ for every $i\in I$. Reflexivity and transitivity follow at each coordinate; if $p\le q\le p$, coordinate antisymmetry gives $p(i)=q(i)$ for every $i$, hence equality of functions. The tuple $\mathbf{1}(i)=1_i$ is a greatest condition with empty support. If $I=\mathrm{\varnothing }$, the product is the singleton consisting of the empty function. A singleton index set recovers its factor. For finite $I$ this is the ordinary full product.

Compatibility, in the sense of Compatibility, ccc and Knaster for posets, is equivalent to coordinatewise compatibility. A common lower bound $r$ gives lower bounds $r(i)$ at all coordinates. Conversely suppose every $p(i),q(i)$ are compatible and put $S=\mathrm{supp}(p)\cup \mathrm{supp}(q)$. For each of the finitely many $i\in S$ select a lower bound $r(i)$; this uses finite existential instantiation, not an infinite choice principle. Set $r(i)=1_i$ off $S$. Then $\mathrm{supp}(r)\subseteq S$, and at coordinates off $S$ both original values are $1_i$. Therefore $r$ belongs to the finite-support product and $r\le p,q$. If $S=\mathrm{\varnothing }$ take $r=\mathbf{1}$. A specified tuple of greatest elements supplies nonemptiness without any choices.