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.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)"
```