equal
deleted
inserted
replaced
4 imports FuncSet Countable_Set |
4 imports FuncSet Countable_Set |
5 begin |
5 begin |
6 |
6 |
7 subsection\<open>Eqpoll\<close> |
7 subsection\<open>Eqpoll\<close> |
8 |
8 |
9 definition eqpoll :: "'a set \<Rightarrow> 'b set \<Rightarrow> bool" (infixl "\<approx>" 50) |
9 definition eqpoll :: "'a set \<Rightarrow> 'b set \<Rightarrow> bool" (infixl \<open>\<approx>\<close> 50) |
10 where "eqpoll A B \<equiv> \<exists>f. bij_betw f A B" |
10 where "eqpoll A B \<equiv> \<exists>f. bij_betw f A B" |
11 |
11 |
12 definition lepoll :: "'a set \<Rightarrow> 'b set \<Rightarrow> bool" (infixl "\<lesssim>" 50) |
12 definition lepoll :: "'a set \<Rightarrow> 'b set \<Rightarrow> bool" (infixl \<open>\<lesssim>\<close> 50) |
13 where "lepoll A B \<equiv> \<exists>f. inj_on f A \<and> f ` A \<subseteq> B" |
13 where "lepoll A B \<equiv> \<exists>f. inj_on f A \<and> f ` A \<subseteq> B" |
14 |
14 |
15 definition lesspoll :: "'a set \<Rightarrow> 'b set \<Rightarrow> bool" (infixl \<open>\<prec>\<close> 50) |
15 definition lesspoll :: "'a set \<Rightarrow> 'b set \<Rightarrow> bool" (infixl \<open>\<prec>\<close> 50) |
16 where "A \<prec> B == A \<lesssim> B \<and> ~(A \<approx> B)" |
16 where "A \<prec> B == A \<lesssim> B \<and> ~(A \<approx> B)" |
17 |
17 |