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





leanprover-community/mathlib,leanprover-community/mathlib