Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] new AFP entry: Cardinality of Set Partitions


view this post on Zulip 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: Mar 28 2024 at 20:16 UTC