Size and number of maximum chains in the poset of SetFamily

Stream: Is there code for X?

[Christoph Spiegel]

Is there any code that tells us that the size of a maximum chain in the poset of subsets of [n] is of size n+1 and that there is a total of n! such chains? If not, would it make sense to PR a proof of these into a (new) Mathlib.Combinatorics.SetFamily.Basic? @Yaël Dillies @Bhavik Mehta (We need it for Lubell's proof of Sperner's Theorem)

[Bhavik Mehta]

As far as I know, we don't have this in mathlib, although I think Yaël might have a construction of a symmetric chain decomposition of the hypercube in LeanCamCombi. Nonetheless, both of the things you mention would be sensible PRs, and I think that location sounds reasonable for now. (Note that we do have Sperner's theorem in mathlib already)

[Bhavik Mehta]

As I look at it again, note that the inequality that Lubell proves is also already in mathlib, and used for Sperner: docs#Finset.sum_card_slice_div_choose_le_one