Commit 2023-05-22 22:49 6f8ab7deView on Github →
feat(combinatorics/set_family/compression/uv): UV-compressing reduces the size of the shadow (#13149)
(∂ (𝓒 u v 𝒜)).card ≤ (∂ 𝒜).card, which is key to Kruskal-Katona.
modified theorem uv.card_compress
modified theorem uv.card_compression
added theorem uv.card_shadow_compression_le
added theorem uv.compress_of_disjoint_of_le'
added theorem uv.compress_sdiff_sdiff
added theorem uv.disjoint_of_mem_compression_of_not_mem
added theorem uv.le_of_mem_compression_of_not_mem
added theorem uv.shadow_compression_subset_compression_shadow
added theorem uv.sup_sdiff_mem_of_mem_compression_of_not_mem