Commit 2022-03-01 17:25 29c84f71

View on Github →

feat(combinatorics/set_family/lym): Lubell-Yamamoto-Meshalkin inequalities (#11248) This proves the two local LYM inequalities, the LYM inequality and Sperner's theorem.

Estimated changes

Created src/combinatorics/set_family/lym.lean

added theorem finset.card_div_choose_le_card_shadow_div_choose

added theorem finset.card_mul_le_card_shadow_mul

added def finset.falling

added theorem finset.falling_zero_subset

added theorem finset.le_card_falling_div_choose

added theorem finset.mem_falling

added theorem finset.sized_falling

added theorem finset.slice_subset_falling

added theorem finset.slice_union_shadow_falling_succ

added theorem finset.sum_card_slice_div_choose_le_one

added theorem is_antichain.disjoint_slice_shadow_falling

added theorem is_antichain.sperner

Modified src/combinatorics/set_family/shadow.lean

added theorem finset.shadow_singleton_empty

added theorem finset.sized_shadow_iff

Modified src/data/finset/basic.lean

added theorem finset.ssubset_iff_exists_insert_subset

added theorem finset.ssubset_iff_exists_subset_erase

Modified src/data/fintype/basic.lean

added theorem finset.insert_inj_on'