Commit 2023-05-22 22:49 6f8ab7de

View on Github →

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.

Estimated changes

Modified src/combinatorics/set_family/compression/uv.lean

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