equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 header {* Cardinal Arithmetic *} |
8 header {* Cardinal Arithmetic *} |
9 |
9 |
10 theory Cardinal_Arithmetic |
10 theory Cardinal_Arithmetic |
11 imports Cardinal_Arithmetic_LFP Cardinal_Order_Relation |
11 imports Cardinal_Arithmetic_FP Cardinal_Order_Relation |
12 begin |
12 begin |
13 |
13 |
14 |
14 |
15 subsection {* Binary sum *} |
15 subsection {* Binary sum *} |
16 |
16 |
175 subsection {* Powerset *} |
175 subsection {* Powerset *} |
176 |
176 |
177 lemma Card_order_cpow: "Card_order (cpow r)" |
177 lemma Card_order_cpow: "Card_order (cpow r)" |
178 unfolding cpow_def by (rule card_of_Card_order) |
178 unfolding cpow_def by (rule card_of_Card_order) |
179 |
179 |
180 lemma Cinfinite_cpow: "Cinfinite r \<Longrightarrow> Cinfinite (cpow r)" |
|
181 unfolding cpow_def cinfinite_def by (metis Field_card_of card_of_Card_order infinite_Pow) |
|
182 |
|
183 lemma cardSuc_ordLeq_cpow: "Card_order r \<Longrightarrow> cardSuc r \<le>o cpow r" |
180 lemma cardSuc_ordLeq_cpow: "Card_order r \<Longrightarrow> cardSuc r \<le>o cpow r" |
184 unfolding cpow_def by (metis Card_order_Pow cardSuc_ordLess_ordLeq card_of_Card_order) |
181 unfolding cpow_def by (metis Card_order_Pow cardSuc_ordLess_ordLeq card_of_Card_order) |
185 |
182 |
186 lemma cpow_cexp_ctwo: "cpow r =o ctwo ^c r" |
183 lemma cpow_cexp_ctwo: "cpow r =o ctwo ^c r" |
187 unfolding cpow_def ctwo_def cexp_def Field_card_of by (rule card_of_Pow_Func) |
184 unfolding cpow_def ctwo_def cexp_def Field_card_of by (rule card_of_Pow_Func) |