Commit 2023-02-03 13:33 009e3ace

View on Github →

feat: port Combinatorics.SetFamily.Compression.UV (#1600)

Estimated changes

Modified Mathlib.lean

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

added def UV.IsCompressed

added theorem UV.card_compress

added theorem UV.card_compression

added def UV.compress

added theorem UV.compress_disjoint

added theorem UV.compress_idem

added theorem UV.compress_mem_compression

added theorem UV.compress_mem_compression_of_mem_compression

added theorem UV.compress_of_disjoint_of_le

added theorem UV.compress_self

added def UV.compression

added theorem UV.compression_idem

added theorem UV.compression_self

added theorem UV.is_compressed_self

added theorem UV.mem_compression

added theorem UV.mem_of_mem_compression

added theorem UV.sup_sdiff_mem_of_mem_compression

added theorem sup_sdiff_injOn