Added vimage_inter_cong
authorhoelzl
Thu, 04 Mar 2010 15:44:06 +0100
changeset 35576 5f6bd3ac99f9
parent 35565 56b070cd7ab3
child 35577 43b93e294522
Added vimage_inter_cong
src/HOL/Set.thy
--- a/src/HOL/Set.thy	Thu Mar 04 11:22:06 2010 +0100
+++ b/src/HOL/Set.thy	Thu Mar 04 15:44:06 2010 +0100
@@ -1656,6 +1656,10 @@
     else if d \<in> A then -B else {})"  
   by (auto simp add: vimage_def) 
 
+lemma vimage_inter_cong:
+  "(\<And> w. w \<in> S \<Longrightarrow> f w = g w) \<Longrightarrow> f -` y \<inter> S = g -` y \<inter> S"
+  by auto
+
 lemma image_Int_subset: "f`(A Int B) <= f`A Int f`B"
 by blast