[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




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.