Cardinality of Set Partitions

The theory’s main theorem states that the cardinality of set parti-tions 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 ’ [1] 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 ’ [2] and Wikipedia [3], and unravels the ful