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.9  by(simp add: card_of_Sigma_ordLeq_infinite)
    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