src/ZF/equalities.thy
changeset 61980 6b780867d426
parent 61798 27f3c10b0b50
child 69593 3dda49e08b9d
     1.1 --- a/src/ZF/equalities.thy	Wed Dec 30 17:38:57 2015 +0100
     1.2 +++ b/src/ZF/equalities.thy	Wed Dec 30 17:45:18 2015 +0100
     1.3 @@ -535,19 +535,19 @@
     1.4  by blast
     1.5  
     1.6  lemma SUM_UN_distrib1:
     1.7 -     "(\<Sigma> x \<in> (\<Union>y\<in>A. C(y)). B(x)) = (\<Union>y\<in>A. \<Sigma> x\<in>C(y). B(x))"
     1.8 +     "(\<Sum>x \<in> (\<Union>y\<in>A. C(y)). B(x)) = (\<Union>y\<in>A. \<Sum>x\<in>C(y). B(x))"
     1.9  by blast
    1.10  
    1.11  lemma SUM_UN_distrib2:
    1.12 -     "(\<Sigma> i\<in>I. \<Union>j\<in>J. C(i,j)) = (\<Union>j\<in>J. \<Sigma> i\<in>I. C(i,j))"
    1.13 +     "(\<Sum>i\<in>I. \<Union>j\<in>J. C(i,j)) = (\<Union>j\<in>J. \<Sum>i\<in>I. C(i,j))"
    1.14  by blast
    1.15  
    1.16  lemma SUM_Un_distrib1:
    1.17 -     "(\<Sigma> i\<in>I \<union> J. C(i)) = (\<Sigma> i\<in>I. C(i)) \<union> (\<Sigma> j\<in>J. C(j))"
    1.18 +     "(\<Sum>i\<in>I \<union> J. C(i)) = (\<Sum>i\<in>I. C(i)) \<union> (\<Sum>j\<in>J. C(j))"
    1.19  by blast
    1.20  
    1.21  lemma SUM_Un_distrib2:
    1.22 -     "(\<Sigma> i\<in>I. A(i) \<union> B(i)) = (\<Sigma> i\<in>I. A(i)) \<union> (\<Sigma> i\<in>I. B(i))"
    1.23 +     "(\<Sum>i\<in>I. A(i) \<union> B(i)) = (\<Sum>i\<in>I. A(i)) \<union> (\<Sum>i\<in>I. B(i))"
    1.24  by blast
    1.25  
    1.26  (*First-order version of the above, for rewriting*)
    1.27 @@ -555,11 +555,11 @@
    1.28  by (rule SUM_Un_distrib2)
    1.29  
    1.30  lemma SUM_Int_distrib1:
    1.31 -     "(\<Sigma> i\<in>I \<inter> J. C(i)) = (\<Sigma> i\<in>I. C(i)) \<inter> (\<Sigma> j\<in>J. C(j))"
    1.32 +     "(\<Sum>i\<in>I \<inter> J. C(i)) = (\<Sum>i\<in>I. C(i)) \<inter> (\<Sum>j\<in>J. C(j))"
    1.33  by blast
    1.34  
    1.35  lemma SUM_Int_distrib2:
    1.36 -     "(\<Sigma> i\<in>I. A(i) \<inter> B(i)) = (\<Sigma> i\<in>I. A(i)) \<inter> (\<Sigma> i\<in>I. B(i))"
    1.37 +     "(\<Sum>i\<in>I. A(i) \<inter> B(i)) = (\<Sum>i\<in>I. A(i)) \<inter> (\<Sum>i\<in>I. B(i))"
    1.38  by blast
    1.39  
    1.40  (*First-order version of the above, for rewriting*)
    1.41 @@ -567,7 +567,7 @@
    1.42  by (rule SUM_Int_distrib2)
    1.43  
    1.44  (*Cf Aczel, Non-Well-Founded Sets, page 115*)
    1.45 -lemma SUM_eq_UN: "(\<Sigma> i\<in>I. A(i)) = (\<Union>i\<in>I. {i} * A(i))"
    1.46 +lemma SUM_eq_UN: "(\<Sum>i\<in>I. A(i)) = (\<Union>i\<in>I. {i} * A(i))"
    1.47  by blast
    1.48  
    1.49  lemma times_subset_iff:
    1.50 @@ -575,7 +575,7 @@
    1.51  by blast
    1.52  
    1.53  lemma Int_Sigma_eq:
    1.54 -     "(\<Sigma> x \<in> A'. B'(x)) \<inter> (\<Sigma> x \<in> A. B(x)) = (\<Sigma> x \<in> A' \<inter> A. B'(x) \<inter> B(x))"
    1.55 +     "(\<Sum>x \<in> A'. B'(x)) \<inter> (\<Sum>x \<in> A. B(x)) = (\<Sum>x \<in> A' \<inter> A. B'(x) \<inter> B(x))"
    1.56  by blast
    1.57  
    1.58  (** Domain **)