Intersecting shadow lemma (source code)

= Intersecting shadow lemma
{title2=$|\partial\mathcal F|\geq|\mathcal F|$}

For an <intersecting family> of $r$-sets with $r\geq1$, its <lower shadow> has at least as many members as the family. Apply <elementary set shifts> and then the <ballot reflection injection> to obtain this bound.