1.1 --- a/src/HOL/Fun.thy	Fri May 20 21:38:32 2011 +0200
     1.2 +++ b/src/HOL/Fun.thy	Fri May 20 21:38:32 2011 +0200
     1.3 @@ -478,6 +478,11 @@
     1.4  lemma surj_image_vimage_eq: "surj f ==> f ` (f -` A) = A"
     1.5  by simp
     1.6  
     1.7 +lemma surj_vimage_empty:
     1.8 +  assumes "surj f" shows "f -` A = {} \<longleftrightarrow> A = {}"
     1.9 +  using surj_image_vimage_eq[OF `surj f`, of A]
    1.10 +  by (intro iffI) fastsimp+
    1.11 +
    1.12  lemma inj_vimage_image_eq: "inj f ==> f -` (f ` A) = A"
    1.13  by (simp add: inj_on_def, blast)
    1.14