Lean: BinaryMatrix.card_toFinsetFamily_le

If \(\mathrm{VCdim}(\mathrm{toFinsetFamily}\, M) \le d\) then \(|\mathrm{toFinsetFamily}\, M| \le \sum _{k = 0}^{d} \binom {n}{k}\). This is the Sauer-Shelah bound [ 17 ] , [ 18 ] , [ 23 ] routed through Mathlib’s Finset.card_shatterer_le_sum_vcDim (Pajor + Sauer-Shelah) into the matrix setting.