New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(combinatorics/set_family/lym): Lubell-Yamamoto-Meshalkin inequalities #11248
Conversation
I think your TODO list is sensible, and would be a great thing to add to the TODO of the new file! In my view, this material is useful without the generalisation, eg Sperner's theorem doesn't generalise to graded orders! |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't really know LYM, but it looks like everything is reasonably designed.
How do we feel about the names local_lym
and lubell_yamamoto_meshalkin
? Unless there's a good reason not to, they probably should be mathlib-ified.
bors r+ |
Pull request successfully merged into master. Build succeeded: |
The lemma `ssubset_iff_exists_insert_subset` was added in #11248 but is just a duplicate of the `ssubset_iff` lemma a few lines earlier in the file. It's only used once. Co-authored-by: Bhavik Mehta <bm489@cam.ac.uk>
This proves the two local LYM inequalities, the LYM inequality and Sperner's theorem.
Co-authored-by: Bhavik Mehta bhavikmehta8@gmail.com
Co-authored-by: Alena Gusakov @agusakov
Most of it could be generalized to grade orders (#11308) but Bhavik and I are of the opinion that this version is worth having either way. I also made sure that the material generalizes easily to graded orders.
finset.slice
and antichain lemmas #11397preorder
andadd_comm_semigroup
#11463insert
is injective and other lemmas #11982