Harper theorem implies the Kruskal-Katona theorem (source code)

= Harper theorem implies the Kruskal-Katona theorem
{c}

Adjoin all lower levels to a <uniform set family> before applying <Harper theorem>. Its remaining neighbourhood contribution is the <upper shadow>, so lexicographic <initial segments> minimize upper shadows. Complementation and reversal of coordinates turn this into <colexicographic order> minimizing the <lower shadow>, giving the <Kruskal-Katona theorem>.