feat(combinatorics/set_family/kruskal_katona): The Kruskal-Katona theorem

[b-mehta]

Prove the Kruskal-Katona theorem and deduce the Erdős–Ko–Rado theorem as a corollary.

---

EDIT: Now ported to Lean 4 in LeanCamCombi

• depends on: [Merged by Bors] - feat(combinatorics/colex): introduce colexicographical order #4858
• depends on: [Merged by Bors] - feat(combinatorics/set_family/shadow): Shadow of a set family #10223
• depends on: [Merged by Bors] - feat(combinatorics/set_family/compression/uv): UV-compression of a set family #10238
• depends on: [Merged by Bors] - feat(combinatorics/set_family/compression/uv): UV-compressing reduces the size of the shadow #13149

[urkud]

@RaitoBezarius I suggest splitting this into a series of much smaller PRs. E.g.,

• add finset.pairwise;
• add finset.all_sized;
• add finset.colex;
• add antichain;
• ...

[b-mehta]

The stuff here can probably go - they let us infer decidability but this can just be done by going classical, so this isn't really necessary

[b-mehta]

I'm assigning this to @agusakov as well who has expressed interest. @RaitoBezarius feel free to work on this too but it's been a while, so you can un-assign yourself if you like.

[RaitoBezarius]

I'm assigning this to @agusakov as well who has expressed interest. @RaitoBezarius feel free to work on this too but it's been a while, so you can un-assign yourself if you like.

I'm definitely okay with letting @agusakov working on this, I will un-assign myself, but I'm still very interested into contributing to mathlib. Just have less time than before unfortunately.

[b-mehta]

No worries, thanks for letting me know! Hope to see your mathlib contributions soon :)

[robertylewis]

@b-mehta @agusakov Great that this seems to be active again. I'm going to change the label to WIP. Note that this PR is very large and it would be best to feed it to reviewers in pieces -- no need to get the whole thing working before making new PRs.

[YaelDillies]

I've ported this to Lean 4 in LeanCamCombi.