170 lemma card_of_Sigma_ordLeq_Cinfinite: |
170 lemma card_of_Sigma_ordLeq_Cinfinite: |
171 "\<lbrakk>Cinfinite r; |I| \<le>o r; \<forall>i \<in> I. |A i| \<le>o r\<rbrakk> \<Longrightarrow> |SIGMA i : I. A i| \<le>o r" |
171 "\<lbrakk>Cinfinite r; |I| \<le>o r; \<forall>i \<in> I. |A i| \<le>o r\<rbrakk> \<Longrightarrow> |SIGMA i : I. A i| \<le>o r" |
172 unfolding cinfinite_def by (blast intro: card_of_Sigma_ordLeq_infinite_Field) |
172 unfolding cinfinite_def by (blast intro: card_of_Sigma_ordLeq_infinite_Field) |
173 |
173 |
174 |
174 |
|
175 lemma card_order_cexp: |
|
176 assumes "card_order r1" "card_order r2" |
|
177 shows "card_order (r1 ^c r2)" |
|
178 proof - |
|
179 have "Field r1 = UNIV" "Field r2 = UNIV" using assms card_order_on_Card_order by auto |
|
180 thus ?thesis unfolding cexp_def Func_def by (simp add: card_of_card_order_on) |
|
181 qed |
|
182 |
|
183 lemma Cinfinite_ordLess_cexp: |
|
184 assumes r: "Cinfinite r" |
|
185 shows "r <o r ^c r" |
|
186 proof - |
|
187 have "r <o ctwo ^c r" using r by (simp only: ordLess_ctwo_cexp) |
|
188 also have "ctwo ^c r \<le>o r ^c r" |
|
189 by (rule cexp_mono1[OF ctwo_ordLeq_Cinfinite]) (auto simp: r ctwo_not_czero Card_order_ctwo) |
|
190 finally show ?thesis . |
|
191 qed |
|
192 |
|
193 lemma infinite_ordLeq_cexp: |
|
194 assumes "Cinfinite r" |
|
195 shows "r \<le>o r ^c r" |
|
196 by (rule ordLess_imp_ordLeq[OF Cinfinite_ordLess_cexp[OF assms]]) |
|
197 |
|
198 |
175 subsection {* Powerset *} |
199 subsection {* Powerset *} |
|
200 |
|
201 definition cpow where "cpow r = |Pow (Field r)|" |
|
202 |
|
203 lemma card_order_cpow: "card_order r \<Longrightarrow> card_order (cpow r)" |
|
204 by (simp only: cpow_def Field_card_order Pow_UNIV card_of_card_order_on) |
|
205 |
|
206 lemma cpow_greater_eq: "Card_order r \<Longrightarrow> r \<le>o cpow r" |
|
207 by (rule ordLess_imp_ordLeq) (simp only: cpow_def Card_order_Pow) |
|
208 |
|
209 lemma Cinfinite_cpow: "Cinfinite r \<Longrightarrow> Cinfinite (cpow r)" |
|
210 unfolding cpow_def cinfinite_def by (metis Field_card_of card_of_Card_order infinite_Pow) |
176 |
211 |
177 lemma Card_order_cpow: "Card_order (cpow r)" |
212 lemma Card_order_cpow: "Card_order (cpow r)" |
178 unfolding cpow_def by (rule card_of_Card_order) |
213 unfolding cpow_def by (rule card_of_Card_order) |
179 |
214 |
180 lemma cardSuc_ordLeq_cpow: "Card_order r \<Longrightarrow> cardSuc r \<le>o cpow r" |
215 lemma cardSuc_ordLeq_cpow: "Card_order r \<Longrightarrow> cardSuc r \<le>o cpow r" |