mathlib

8bd20598 - feat(data/finset/slice): `r`-sets and slice (#10685)

feat(data/finset/slice): `r`-sets and slice (#10685) Two simple nonetheless useful definitions about set families. A family of `r`-sets is a set of finsets of cardinality `r`. The slice of a set family is its subset of `r`-sets.