Theorem Finset.card_biUnion_le_card_mul

Modification history