Commit 2025-03-27 12:28 da234f84

View on Github →

feat: other form of the LYM inequality (#22633) and use semantic names for the existing lemmas. Moves:

card_mul_le_card_shadow_mul → local_lubell_yamamoto_meshalkin_inequality_mul
card_div_choose_le_card_shadow_div_choose → local_lubell_yamamoto_meshalkin_inequality_div
sum_card_slice_div_choose_le_one → lubell_yamamoto_meshalkin_inequality_sum_card_div_choose From PlainCombi (LeanCamCombi)

Estimated changes

Modified Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean

Modified Mathlib/Combinatorics/SetFamily/LYM.lean

deleted theorem Finset.card_div_choose_le_card_shadow_div_choose

deleted theorem Finset.card_mul_le_card_shadow_mul

added theorem Finset.local_lubell_yamamoto_meshalkin_inequality_div

added theorem Finset.local_lubell_yamamoto_meshalkin_inequality_mul

added theorem Finset.lubell_yamamoto_meshalkin_inequality_sum_card_div_choose

added theorem Finset.lubell_yamamoto_meshalkin_inequality_sum_inv_choose

deleted theorem Finset.sum_card_slice_div_choose_le_one

modified theorem IsAntichain.sperner

Modified docs/overview.yaml