Antichain trace bound for intersection-free families (source code)

= Antichain trace bound for intersection-free families
{title2=$|\mathcal F|\leq1+\binom r{\lfloor r/2\rfloor}$}

For an <intersection-free uniform set family> of rank $r$, fix $X\in\mathcal F$. The map $A\mapsto X\cap A$ on $\mathcal F\setminus\{X\}$ is injective and its image is an <antichain> in $\mathcal P(X)$: a containment $X\cap A\subseteq X\cap B$ would violate intersection-freeness on the distinct members $X,A,B$. The <Sperner theorem> then proves the displayed bound.