[isabelle] new AFP entry: Cardinality of Set Partitions
- To: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>
- Subject: [isabelle] new AFP entry: Cardinality of Set Partitions
- From: Gerwin Klein <Gerwin.Klein at nicta.com.au>
- Date: Sun, 13 Dec 2015 09:53:34 +0000
- Accept-language: en-AU, en-US
- Thread-index: AQHRNYwhCIAEZHzQb0Gk4134HbF3yQ==
- Thread-topic: 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
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