Disjoint occurrence of increasing events (source code)

= Disjoint occurrence of increasing events
{title2=$A\mathbin\square B$}

A finite open coordinate <set> witnesses an <increasing event> when prescribing those coordinates open forces the event, regardless of the remaining configuration. The <disjoint occurrence of increasing events> $A\square B$ means that $A$ and $B$ have disjoint finite witnesses. For finite-coordinate events this is the usual disjoint-occurrence definition. The <van den Berg-Kesten inequality> bounds its <probability> by $\mathbb P(A)\mathbb P(B)$ under an independent <Bernoulli distribution> <product measure>.