equal
deleted
inserted
replaced
8 |
8 |
9 section \<open>Bijections of a Set, Permutation and Automorphism Groups\<close> |
9 section \<open>Bijections of a Set, Permutation and Automorphism Groups\<close> |
10 |
10 |
11 definition |
11 definition |
12 Bij :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) set" |
12 Bij :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) set" |
13 --\<open>Only extensional functions, since otherwise we get too many.\<close> |
13 \<comment>\<open>Only extensional functions, since otherwise we get too many.\<close> |
14 where "Bij S = extensional S \<inter> {f. bij_betw f S S}" |
14 where "Bij S = extensional S \<inter> {f. bij_betw f S S}" |
15 |
15 |
16 definition |
16 definition |
17 BijGroup :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) monoid" |
17 BijGroup :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) monoid" |
18 where "BijGroup S = |
18 where "BijGroup S = |