src/ZF/equalities.ML
 changeset 192 3dc5c8016a0e parent 182 e30b55c07235 child 198 0f0ff91b07f6
```--- a/src/ZF/equalities.ML	Fri Dec 10 10:36:39 1993 +0100
+++ b/src/ZF/equalities.ML	Fri Dec 10 10:39:12 1993 +0100
@@ -217,13 +217,13 @@
(** Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5:
Union of a family of unions **)

-goal ZF.thy "(UN i:I. A(x) Un B(x)) = (UN i:I. A(x))  Un  (UN i:I. B(x))";
+goal ZF.thy "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i))  Un  (UN i:I. B(i))";
by (fast_tac eq_cs 1);
val UN_Un_distrib = result();

goal ZF.thy
"!!A B. i:I ==> \
-\           (INT i:I. A(x)  Int  B(x)) = (INT i:I. A(x)) Int (INT i:I. B(x))";
+\           (INT i:I. A(i)  Int  B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))";
by (fast_tac eq_cs 1);
val INT_Int_distrib = result();

@@ -243,28 +243,32 @@
by (fast_tac eq_cs 1);
val SUM_UN_distrib1 = result();

-goal ZF.thy "(SUM x:A. UN y:B. C(x,y)) = (UN y:B. SUM x:A. C(x,y))";
+goal ZF.thy "(SUM i:I. UN j:J. C(i,j)) = (UN j:J. SUM i:I. C(i,j))";
by (fast_tac eq_cs 1);
val SUM_UN_distrib2 = result();

-goal ZF.thy "(SUM x:A Un B. C(x)) = (SUM x:A. C(x)) Un (SUM x:B. C(x))";
+goal ZF.thy "(SUM i:I Un J. C(i)) = (SUM i:I. C(i)) Un (SUM j:J. C(j))";
by (fast_tac eq_cs 1);
val SUM_Un_distrib1 = result();

-goal ZF.thy
-    "(SUM i:I. A(x) Un B(x)) = (SUM i:I. A(x)) Un (SUM i:I. B(x))";
+goal ZF.thy "(SUM i:I. A(i) Un B(i)) = (SUM i:I. A(i)) Un (SUM i:I. B(i))";
by (fast_tac eq_cs 1);
val SUM_Un_distrib2 = result();

-goal ZF.thy "(SUM x:A Int B. C(x)) = (SUM x:A. C(x)) Int (SUM x:B. C(x))";
+goal ZF.thy "(SUM i:I Int J. C(i)) = (SUM i:I. C(i)) Int (SUM j:J. C(j))";
by (fast_tac eq_cs 1);
val SUM_Int_distrib1 = result();

goal ZF.thy
-    "(SUM i:I. A(x) Int B(x)) = (SUM i:I. A(x)) Int (SUM i:I. B(x))";
+    "(SUM i:I. A(i) Int B(i)) = (SUM i:I. A(i)) Int (SUM i:I. B(i))";
by (fast_tac eq_cs 1);
val SUM_Int_distrib2 = result();

+(*Cf Aczel, Non-Well-Founded Sets, page 115*)
+goal ZF.thy "(SUM i:I. A(i)) = (UN i:I. {i} * A(i))";
+by (fast_tac eq_cs 1);
+val SUM_eq_UN = result();
+
(** Domain, Range and Field **)

goal ZF.thy "domain(A Un B) = domain(A) Un domain(B)";```