Theorem UV.compress_of_disjoint_of_le'

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.compress_of_disjoint_of_le'View on Github →