Commit 2023-02-02 11:17 00ef5796

View on Github →

feat: port Combinatorics.SetFamily.LYM (#1969)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/SetFamily/LYM.lean

added theorem Finset.IsAntichain.disjoint_slice_shadow_falling

added theorem Finset.IsAntichain.sperner

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