equal
deleted
inserted
replaced
23 definition |
23 definition |
24 lesspoll :: "[i,i] \<Rightarrow> o" (infixl \<open>\<prec>\<close> 50) where |
24 lesspoll :: "[i,i] \<Rightarrow> o" (infixl \<open>\<prec>\<close> 50) where |
25 "A \<prec> B \<equiv> A \<lesssim> B \<and> \<not>(A \<approx> B)" |
25 "A \<prec> B \<equiv> A \<lesssim> B \<and> \<not>(A \<approx> B)" |
26 |
26 |
27 definition |
27 definition |
28 cardinal :: "i\<Rightarrow>i" (\<open>|_|\<close>) where |
28 cardinal :: "i\<Rightarrow>i" (\<open>(\<open>open_block notation=\<open>mixfix cardinal\<close>\<close>|_|)\<close>) |
29 "|A| \<equiv> (\<mu> i. i \<approx> A)" |
29 where "|A| \<equiv> (\<mu> i. i \<approx> A)" |
30 |
30 |
31 definition |
31 definition |
32 Finite :: "i\<Rightarrow>o" where |
32 Finite :: "i\<Rightarrow>o" where |
33 "Finite(A) \<equiv> \<exists>n\<in>nat. A \<approx> n" |
33 "Finite(A) \<equiv> \<exists>n\<in>nat. A \<approx> n" |
34 |
34 |