# HG changeset patch # User hoelzl # Date 1267713846 -3600 # Node ID 5f6bd3ac99f95970794f624350b75fb15efe99d0 # Parent 56b070cd7ab3236b0f126ec9b408f78ae07260b4 Added vimage_inter_cong diff -r 56b070cd7ab3 -r 5f6bd3ac99f9 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 \ A then -B else {})" by (auto simp add: vimage_def) +lemma vimage_inter_cong: + "(\ w. w \ S \ f w = g w) \ f -` y \ S = g -` y \ S" + by auto + lemma image_Int_subset: "f`(A Int B) <= f`A Int f`B" by blast