Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finset.le_truncated_sup

Modification history

2023-09-12 13:12

src/combinatorics/set_family/ahlswede_zhang.lean

feat(combinatorics/set_family/ahlswede_zhang): Ahlswede-Zhang identity, part I (#18612) …

Added finset.le_truncated_sup View on Github →