src/HOL/Cardinals/Cardinal_Order_Relation.thy
 changeset 61943 7fba644ed827 parent 60585 48fdff264eb2 child 61952 546958347e05
```     1.1 --- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Sun Dec 27 21:46:36 2015 +0100
1.2 +++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Sun Dec 27 22:07:17 2015 +0100
1.3 @@ -489,7 +489,7 @@
1.4
1.5  lemma card_of_Times_ordLeq_infinite:
1.6  "\<lbrakk>\<not>finite C; |A| \<le>o |C|; |B| \<le>o |C|\<rbrakk>
1.7 - \<Longrightarrow> |A <*> B| \<le>o |C|"
1.8 + \<Longrightarrow> |A \<times> B| \<le>o |C|"
1.10
1.11  corollary Plus_infinite_bij_betw:
1.12 @@ -621,7 +621,7 @@
1.13    ordIso_symmetric by blast
1.14    hence "|A| <o |?C|"  "|B| <o |?C|"
1.15    using LESS1 LESS2 ordLess_ordIso_trans by blast+
1.16 -  hence  "|A <*> B| <o |?C|" using INF
1.17 +  hence  "|A \<times> B| <o |?C|" using INF
1.18    card_of_Times_ordLess_infinite by blast
1.19    thus ?thesis using 1 ordLess_ordIso_trans by blast
1.20  qed
1.21 @@ -1502,12 +1502,12 @@
1.22
1.23  lemma card_of_Pfunc_Pow_Func_option:
1.24  assumes "B \<noteq> {}"
1.25 -shows "|Pfunc A B| \<le>o |Pow A <*> Func_option A B|"
1.26 +shows "|Pfunc A B| \<le>o |Pow A \<times> Func_option A B|"
1.27  proof-
1.28    have "|Pfunc A B| =o |\<Union>A' \<in> Pow A. Func_option A' B|" (is "_ =o ?K")
1.29      unfolding Pfunc_Func_option by(rule card_of_refl)
1.30    also have "?K \<le>o |Sigma (Pow A) (\<lambda> A'. Func_option A' B)|" using card_of_UNION_Sigma .
1.31 -  also have "|Sigma (Pow A) (\<lambda> A'. Func_option A' B)| \<le>o |Pow A <*> Func_option A B|"
1.32 +  also have "|Sigma (Pow A) (\<lambda> A'. Func_option A' B)| \<le>o |Pow A \<times> Func_option A B|"
1.33      apply(rule card_of_Sigma_mono1) using card_of_Func_option_mono[OF _ assms] by auto
1.34    finally show ?thesis .
1.35  qed
```