Colexicographic section compression (source code)

= Colexicographic section compression
{title2=$C_i^{\mathrm{colex}}$}

Split a <uniform set family> into the section avoiding a coordinate and the section containing it, with that coordinate removed. Replace each section by a <colexicographic initial segment> of the same size. Induction on the ground-set size, and nesting of initial segments, show that this operation cannot enlarge the <lower shadow>.