changeset 51173 | 3cbb4e95a565 |
parent 50580 | fbb973a53106 |
child 51334 | fd531bd984d8 |
--- a/src/HOL/Set.thy Sun Feb 17 20:45:49 2013 +0100 +++ b/src/HOL/Set.thy Sun Feb 17 21:29:30 2013 +0100 @@ -908,6 +908,10 @@ -- {* The eta-expansion gives variable-name preservation. *} by (unfold image_def) blast +lemma Compr_image_eq: + "{x \<in> f ` A. P x} = f ` {x \<in> A. P (f x)}" + by auto + lemma image_Un: "f`(A Un B) = f`A Un f`B" by blast