equal
deleted
inserted
replaced
454 subsection \<open>The Alephs\<close> |
454 subsection \<open>The Alephs\<close> |
455 text \<open>This is the well-known transfinite enumeration of the cardinal |
455 text \<open>This is the well-known transfinite enumeration of the cardinal |
456 numbers.\<close> |
456 numbers.\<close> |
457 |
457 |
458 definition |
458 definition |
459 Aleph :: "i => i" ("\<aleph>_" [90] 90) where |
459 Aleph :: "i => i" (\<open>\<aleph>_\<close> [90] 90) where |
460 "Aleph(a) == transrec2(a, nat, \<lambda>x r. csucc(r))" |
460 "Aleph(a) == transrec2(a, nat, \<lambda>x r. csucc(r))" |
461 |
461 |
462 lemma Card_Aleph [simp, intro]: |
462 lemma Card_Aleph [simp, intro]: |
463 "Ord(a) ==> Card(Aleph(a))" |
463 "Ord(a) ==> Card(Aleph(a))" |
464 apply (erule trans_induct3) |
464 apply (erule trans_induct3) |