equal
deleted
inserted
replaced
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 "~~/src/HOL/Binomial" "~~/src/HOL/Library/FuncSet" |
8 imports Main HOL.Binomial "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: |