Commit 2023-10-17 07:52 0b9b714c

View on Github →

chore: Fix decidability issues in UV-compression (#7708) We had been a bit lazy in Lean 3 with the decidability instances here, and it recently bit me. This PR reorders the lemmas to avoid decidableEqOfDecidableLE. There's only one new lemma: Set.Sized.uvCompression. Also golf a bit and fix style.

Estimated changes

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

added theorem Set.Sized.uvCompression

modified theorem UV.compress_disjoint

added theorem UV.compress_injOn

modified theorem UV.compression_idem

added theorem UV.isCompressed_self

deleted theorem UV.is_compressed_self

modified theorem UV.sup_sdiff_mem_of_mem_compression