Counting set partitions of a finset

A finset s in a linear order has at most #s ^ #s set partitions (Fintype.card_finpartition_le): a set partition is determined by the map sending each element of s to the largest element of its part.

Main results

• Fintype.card_finpartition_le: Fintype.card (Finpartition s) ≤ #s ^ #s.

References

The bound is standard and its proof is original. The Bell number B_n counts the set partitions of an n-element set; the bound here is the crude B_n ≤ n ^ n.

theorem Fintype.card_finpartition_le {α : Type u_1} [LinearOrder α] (s : Finset α) : card (Finpartition s) ≤ s.card ^ s.card

The number of set partitions (standard bound, proof original): a finset s in a linear order has at most #s ^ #s set partitions. A set partition is determined by the largest element of the part of each point.