mathlib3

1dd3ae1c - feat(algebra/big_operators/order): Bounding on a sum of cards by double counting (#10389)

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`.