# Cardinality of Set Partitions

 Title: Cardinality of Set Partitions Author: Lukas Bulwahn (lukas /dot/ bulwahn /at/ gmail /dot/ com) Submission date: 2015-12-12 Abstract: 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. BibTeX: @article{Card_Partitions-AFP, author = {Lukas Bulwahn}, title = {Cardinality of Set Partitions}, journal = {Archive of Formal Proofs}, month = dec, year = 2015, note = {\url{http://isa-afp.org/entries/Card_Partitions.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Depends on: Discrete_Summation Used by: Bell_Numbers_Spivey, Falling_Factorial_Sum, Twelvefold_Way Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.