src/HOL/Analysis/Binary_Product_Measure.thy
changeset 69313 b021008c5397
parent 69260 0a9688695a1b
child 69517 dc20f278e8f3
     1.1 --- a/src/HOL/Analysis/Binary_Product_Measure.thy	Sun Nov 18 09:51:41 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Binary_Product_Measure.thy	Sun Nov 18 18:07:51 2018 +0000
     1.3 @@ -1118,7 +1118,7 @@
     1.4          unfolding * by auto
     1.5      next
     1.6        case (Union A)
     1.7 -      moreover have *: "(UNION UNIV A) \<times> UNIV = UNION UNIV (\<lambda>i. A i \<times> UNIV)"
     1.8 +      moreover have *: "(\<Union>(A ` UNIV)) \<times> UNIV = \<Union>((\<lambda>i. A i \<times> UNIV) ` UNIV)"
     1.9          by auto
    1.10        ultimately show ?case
    1.11          unfolding * by auto
    1.12 @@ -1137,7 +1137,7 @@
    1.13          unfolding * by auto
    1.14      next
    1.15        case (Union B)
    1.16 -      moreover have *: "UNIV \<times> (UNION UNIV B) = UNION UNIV (\<lambda>i. UNIV \<times> B i)"
    1.17 +      moreover have *: "UNIV \<times> (\<Union>(B ` UNIV)) = \<Union>((\<lambda>i. UNIV \<times> B i) ` UNIV)"
    1.18          by auto
    1.19        ultimately show ?case
    1.20          unfolding * by auto