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.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.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.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.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.26  (*First-order version of the above, for rewriting*)
1.27 @@ -555,11 +555,11 @@
1.28  by (rule SUM_Un_distrib2)
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.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.40  (*First-order version of the above, for rewriting*)
1.41 @@ -567,7 +567,7 @@
1.42  by (rule SUM_Int_distrib2)
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.49  lemma times_subset_iff:
1.50 @@ -575,7 +575,7 @@
1.51  by blast
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.58  (** Domain **)