Sperner theorem

Every antichain in $\mathcal{P}([n])$ has at most $\left(\genfrac{}{}{0ex}{}{n}{\lfloor n/2\rfloor }\right)$ members. Equality is attained only by a full middle level, with either middle level possible when $n$ is odd.