author | hoelzl |
Thu, 04 Mar 2010 15:44:06 +0100 | |
changeset 35576 | 5f6bd3ac99f9 |
parent 35565 | 56b070cd7ab3 |
child 35577 | 43b93e294522 |
src/HOL/Set.thy | file | annotate | diff | comparison | revisions |
--- 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