| changeset 68188 | 2af1f142f855 |
| parent 68072 | 493b818e8e10 |
| 68187:48262e3a2bde | 68188:2af1f142f855 |
|---|---|
3 *) |
3 *) |
4 |
4 |
5 section \<open>A Formulation of the Birthday Paradox\<close> |
5 section \<open>A Formulation of the Birthday Paradox\<close> |
6 |
6 |
7 theory Birthday_Paradox |
7 theory Birthday_Paradox |
8 imports Main HOL.FuncSet |
8 imports Main "HOL-Library.FuncSet" |
9 begin |
9 begin |
10 |
10 |
11 section \<open>Cardinality\<close> |
11 section \<open>Cardinality\<close> |
12 |
12 |
13 lemma card_product_dependent: |
13 lemma card_product_dependent: |