Cardinality of Set Partitions

Lukas Bulwahn 📧

December 12, 2015

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


The theory's main theorem states that the cardinality of set partitions of size k on a carrier set of size n is expressed by Stirling numbers of the second kind. In Isabelle, Stirling numbers of the second kind are defined in the AFP entry `Discrete Summation` through their well-known recurrence relation. The main theorem relates them to the alternative definition as cardinality of set partitions. The proof follows the simple and short explanation in Richard P. Stanley's `Enumerative Combinatorics: Volume 1` and Wikipedia, and unravels the full details and implicit reasoning steps of these explanations.


BSD License


Session Card_Partitions