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, Twelvefold_Way