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.