Families compressed in every binary section (source code)

= Families compressed in every binary section

If both sections for every coordinate are <binary initial segments>, then the family itself is a binary initial segment, apart from the possible family $(\mathcal P([n-1])\setminus\{[n-1]\})\cup\{\{n\}\}$. Any missing vertex earlier than a present vertex must disagree with it in every coordinate; the two are therefore complementary and consecutive in <binary order on the discrete cube>, forcing this sole exceptional shape.