Commit 2023-06-05 05:24 1ead7462

View on Github →

feat: UV-compressing reduces the size of the shadow (#4546) Match https://github.com/leanprover-community/mathlib/pull/13149 combinatorics.set_family.compression.uv@9003f28797c0664a49e4179487267c494477d853..6f8ab7de1c4b78a68ab8cf7dd83d549eb78a68a1

Estimated changes

Modified Mathlib/Combinatorics/SetFamily/Compression/UV.lean

modified theorem UV.card_compress

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