src/HOL/BNF_Cardinal_Order_Relation.thy
changeset 61943 7fba644ed827
parent 61799 4cf66f21b764
child 62343 24106dc44def
     1.1 --- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Sun Dec 27 21:46:36 2015 +0100
     1.2 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Sun Dec 27 22:07:17 2015 +0100
     1.3 @@ -788,7 +788,7 @@
     1.4  qed
     1.5  
     1.6  lemma card_of_Times_Plus_distrib:
     1.7 -  "|A <*> (B <+> C)| =o |A <*> B <+> A <*> C|" (is "|?RHS| =o |?LHS|")
     1.8 +  "|A \<times> (B <+> C)| =o |A \<times> B <+> A \<times> C|" (is "|?RHS| =o |?LHS|")
     1.9  proof -
    1.10    let ?f = "\<lambda>(a, bc). case bc of Inl b \<Rightarrow> Inl (a, b) | Inr c \<Rightarrow> Inr (a, c)"
    1.11    have "bij_betw ?f ?RHS ?LHS" unfolding bij_betw_def inj_on_def by force
    1.12 @@ -1038,7 +1038,7 @@
    1.13  
    1.14  lemma card_of_Times_ordLeq_infinite_Field:
    1.15  "\<lbrakk>\<not>finite (Field r); |A| \<le>o r; |B| \<le>o r; Card_order r\<rbrakk>
    1.16 - \<Longrightarrow> |A <*> B| \<le>o r"
    1.17 + \<Longrightarrow> |A \<times> B| \<le>o r"
    1.18  by(simp add: card_of_Sigma_ordLeq_infinite_Field)
    1.19  
    1.20  lemma card_of_Times_infinite_simps:
    1.21 @@ -1619,7 +1619,7 @@
    1.22  subsection \<open>Others\<close>
    1.23  
    1.24  lemma card_of_Func_Times:
    1.25 -"|Func (A <*> B) C| =o |Func A (Func B C)|"
    1.26 +"|Func (A \<times> B) C| =o |Func A (Func B C)|"
    1.27  unfolding card_of_ordIso[symmetric]
    1.28  using bij_betw_curr by blast
    1.29  
    1.30 @@ -1661,7 +1661,7 @@
    1.31  qed
    1.32  
    1.33  lemma Func_Times_Range:
    1.34 -  "|Func A (B <*> C)| =o |Func A B <*> Func A C|" (is "|?LHS| =o |?RHS|")
    1.35 +  "|Func A (B \<times> C)| =o |Func A B \<times> Func A C|" (is "|?LHS| =o |?RHS|")
    1.36  proof -
    1.37    let ?F = "\<lambda>fg. (\<lambda>x. if x \<in> A then fst (fg x) else undefined,
    1.38                    \<lambda>x. if x \<in> A then snd (fg x) else undefined)"