Intersection-preserving lexicographic UV-compression (source code)

= Intersection-preserving lexicographic UV-compression

Let $U,V$ be disjoint, equally sized, nonempty <sets>, with $\min U<\min V$. Suppose an <intersecting family> is unchanged by all such <UV-compressions> of smaller size. Then its $(U,V)$-<UV-compression> is still an <intersecting family>. Indeed, a newly moved member $A'=(A\setminus V)\cup U$ can only be disjoint from a retained old member $B$, since two newly moved members share $U$. Here $B\cap U=\varnothing$ and $V'=B\cap V\ne\varnothing$. If $V'=V$, retaining $B$ forces $(B\setminus V)\cup U$ to have been present, contradicting the old <intersection> property with $A$. Otherwise choose $U'\subset U$ with $|U'|=|V'|$ and $\min U\in U'$. Stability under the smaller $(U',V')$-<UV-compression> forces $(A\setminus V')\cup U'$ to be present; this member is disjoint from $B$, again a contradiction. Repeatedly applying a changing <UV-compression> of smallest size terminates, since the sum of <lexicographic order> positions decreases. A terminal <set family> is a <lexicographic> initial segment: a missing earlier member $X$ and present later member $Y$ would be moved by $U=X\setminus Y$, $V=Y\setminus X$.