Commit 2021-11-23 18:21 1dd3ae1c

feat(algebra/big_operators/order): Bounding on a sum of cards by double counting (#10389) If every element of s is in at least/most n finsets of B : finset (finset α), then the sum of (s ∩ t).card over t ∈ B is at most/least s.card * n.