mathlib

6f8ab7de - feat(combinatorics/set_family/compression/uv): UV-compressing reduces the size of the shadow (#13149)

feat(combinatorics/set_family/compression/uv): UV-compressing reduces the size of the shadow (#13149) Prove `(∂ (𝓒 u v 𝒜)).card ≤ (∂ 𝒜).card`, which is key to Kruskal-Katona. Co-authored-by: Bhavik Mehta <bhavik.mehta8@gmail.com> Co-authored-by: Mauricio Collares <mauricio@collares.org> Co-authored-by: Eric Rodriguez <ericrboidi@gmail.com>