Email Gateway (Aug 22 2022 at 12:01): Email Gateway (Aug 22 2022 at 12:01):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
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.
Last updated: Nov 21 2024 at 12:39 UTC