Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finset.card_truncated_sup_union_add_card_truncated_sup_infs

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