# HG changeset patch
# User hoelzl
# Date 1305920312 -7200
# Node ID ec9eb1fbfcb88e3c08c9532ea09a5aa81046337e
# Parent  e8dbf90a2f3ba7514c8acc1b3fcae294c5f90422
add surj_vimage_empty

diff -r e8dbf90a2f3b -r ec9eb1fbfcb8 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Fri May 20 21:38:32 2011 +0200
+++ b/src/HOL/Fun.thy	Fri May 20 21:38:32 2011 +0200
@@ -478,6 +478,11 @@
 lemma surj_image_vimage_eq: "surj f ==> f ` (f -` A) = A"
 by simp
 
+lemma surj_vimage_empty:
+  assumes "surj f" shows "f -` A = {} \<longleftrightarrow> A = {}"
+  using surj_image_vimage_eq[OF `surj f`, of A]
+  by (intro iffI) fastsimp+
+
 lemma inj_vimage_image_eq: "inj f ==> f -` (f ` A) = A"
 by (simp add: inj_on_def, blast)