Connectedness of adjacent-level incidence in a Boolean lattice (source code)

= Connectedness of adjacent-level incidence in a Boolean lattice
{title2=$[n]^{(r)}\longleftrightarrow[n]^{(r+1)}$}

The bipartite inclusion <graph> between consecutive nonempty ranks of the <Boolean lattice> is connected. Two rank-$r$ sets differing by one exchanged element share their rank-$(r+1)$ union as a neighbour; successive exchanges connect any two rank-$r$ sets. Every upper vertex has a lower neighbour. For the two middle ranks of an odd-dimensional <Boolean lattice> the <graph> is regular, so equality in the <Local LYM inequality> for a nonempty upper family forces the whole upper rank: equality admits no <edges> from its <lower shadow> to the remaining upper <vertices>.