src/HOL/BNF_Cardinal_Order_Relation.thy
changeset 60585 48fdff264eb2
parent 58889 5b7a9633cfa8
child 60758 d8d85a8172b5
     1.1 --- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Fri Jun 26 00:14:10 2015 +0200
     1.2 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Fri Jun 26 10:20:33 2015 +0200
     1.3 @@ -1051,10 +1051,10 @@
     1.4  lemma card_of_UNION_ordLeq_infinite:
     1.5  assumes INF: "\<not>finite B" and
     1.6          LEQ_I: "|I| \<le>o |B|" and LEQ: "\<forall>i \<in> I. |A i| \<le>o |B|"
     1.7 -shows "|\<Union> i \<in> I. A i| \<le>o |B|"
     1.8 +shows "|\<Union>i \<in> I. A i| \<le>o |B|"
     1.9  proof(cases "I = {}", simp add: card_of_empty)
    1.10    assume *: "I \<noteq> {}"
    1.11 -  have "|\<Union> i \<in> I. A i| \<le>o |SIGMA i : I. A i|"
    1.12 +  have "|\<Union>i \<in> I. A i| \<le>o |SIGMA i : I. A i|"
    1.13    using card_of_UNION_Sigma by blast
    1.14    moreover have "|SIGMA i : I. A i| \<le>o |B|"
    1.15    using assms card_of_Sigma_ordLeq_infinite by blast
    1.16 @@ -1064,14 +1064,14 @@
    1.17  corollary card_of_UNION_ordLeq_infinite_Field:
    1.18  assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and
    1.19          LEQ_I: "|I| \<le>o r" and LEQ: "\<forall>i \<in> I. |A i| \<le>o r"
    1.20 -shows "|\<Union> i \<in> I. A i| \<le>o r"
    1.21 +shows "|\<Union>i \<in> I. A i| \<le>o r"
    1.22  proof-
    1.23    let ?B  = "Field r"
    1.24    have 1: "r =o |?B| \<and> |?B| =o r" using r card_of_Field_ordIso
    1.25    ordIso_symmetric by blast
    1.26    hence "|I| \<le>o |?B|"  "\<forall>i \<in> I. |A i| \<le>o |?B|"
    1.27    using LEQ_I LEQ ordLeq_ordIso_trans by blast+
    1.28 -  hence  "|\<Union> i \<in> I. A i| \<le>o |?B|" using INF LEQ
    1.29 +  hence  "|\<Union>i \<in> I. A i| \<le>o |?B|" using INF LEQ
    1.30    card_of_UNION_ordLeq_infinite by blast
    1.31    thus ?thesis using 1 ordLeq_ordIso_trans by blast
    1.32  qed