Theorem UV.le_of_mem_compression_of_not_mem

Modification history

2023-06-05 05:24
Mathlib/Combinatorics/SetFamily/Compression/UV.lean
feat: UV-compressing reduces the size of the shadow (#4546) …
Added UV.le_of_mem_compression_of_not_memView on Github →