[isabelle] new AFP entry: Cardinality of Set Partitions



Cardinality of Set Partitions
by Lukas Bulwahn

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.

[http://afp.sf.net/entries/Card_Partitions.shtml]


Enjoy!
Gerwin

________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.