Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-02 14:23 790d6373

View on Github →

feat(combinatorics/set_family/compression/uv): UV-compression of a set family (#10238) This defines the UV-compression of a set family, along with a bunch of preliminary definitions and some basic results.

Estimated changes

added theorem sup_sdiff_inj_on
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_self
added def uv.compression
added theorem uv.compression_idem
added theorem uv.compression_self
added def uv.is_compressed
added theorem uv.is_compressed_self
added theorem uv.mem_compression
added theorem le_sdiff_iff