equal
deleted
inserted
replaced
1047 by auto |
1047 by auto |
1048 |
1048 |
1049 lemma UN_insert_distrib: "u \<in> A ==> (\<Union>x\<in>A. insert a (B x)) = insert a (\<Union>x\<in>A. B x)" |
1049 lemma UN_insert_distrib: "u \<in> A ==> (\<Union>x\<in>A. insert a (B x)) = insert a (\<Union>x\<in>A. B x)" |
1050 by blast |
1050 by blast |
1051 |
1051 |
|
1052 lemma insert_disjoint[simp]: |
|
1053 "(insert a A \<inter> B = {}) = (a \<notin> B \<and> A \<inter> B = {})" |
|
1054 by blast |
|
1055 |
|
1056 lemma disjoint_insert[simp]: |
|
1057 "(B \<inter> insert a A = {}) = (a \<notin> B \<and> B \<inter> A = {})" |
|
1058 by blast |
1052 |
1059 |
1053 text {* \medskip @{text image}. *} |
1060 text {* \medskip @{text image}. *} |
1054 |
1061 |
1055 lemma image_empty [simp]: "f`{} = {}" |
1062 lemma image_empty [simp]: "f`{} = {}" |
1056 by blast |
1063 by blast |