State the set family results

Many results from [lectures 1 to 9](https://github.com/YaelDillies/maths-notes/blob/master/combinatorics.pdf) are already in Mathlib and can readily be stated and proved from the Mathlib versions.