### Abstract

This entry provides all cardinality theorems of the Twelvefold Way. The Twelvefold Way systematically classifies twelve related combinatorial problems concerning two finite sets, which include counting permutations, combinations, multisets, set partitions and number partitions. This development builds upon the existing formal developments with cardinality theorems for those structures. It provides twelve bijections from the various structures to different equivalence classes on finite functions, and hence, proves cardinality formulae for these equivalence classes on finite functions.

### License

BSD License

### Topics

- Mathematics/Combinatorics

### Session Twelvefold_Way

- Preliminaries
- Twelvefold_Way_Core
- Equiv_Relations_on_Functions
- Twelvefold_Way_Entry1
- Twelvefold_Way_Entry2
- Twelvefold_Way_Entry4
- Twelvefold_Way_Entry5
- Twelvefold_Way_Entry6
- Twelvefold_Way_Entry7
- Twelvefold_Way_Entry8
- Twelvefold_Way_Entry9
- Twelvefold_Way_Entry3
- Twelvefold_Way_Entry10
- Twelvefold_Way_Entry11
- Twelvefold_Way_Entry12
- Card_Bijections
- Card_Bijections_Direct
- Twelvefold_Way

### Depends on

- Spivey’s Generalized Recurrence for Bell Numbers
- Cardinality of Multisets
- Cardinality of Number Partitions
- Cardinality of Set Partitions

### Used by

- Hypergraph Colouring Bounds

### Auto-related entries

- Myhill-Nerode Theorem for Nominal G-Automata

## Cite

×

Twelvefold_Way-AFP

    @article{Twelvefold_Way-AFP,
      author  = {Lukas Bulwahn},
      title   = {The Twelvefold Way},
      journal = {Archive of Formal Proofs},
      month   = {December},
      year    = {2016},
      note    = {\url{https://isa-afp.org/entries/Twelvefold_Way.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 30, 2016 : Isabelle2016-1