author | hoelzl |
Fri, 20 May 2011 21:38:32 +0200 | |
changeset 42903 | ec9eb1fbfcb8 |
parent 42902 | e8dbf90a2f3b |
child 42904 | 4aedcff42de6 |
src/HOL/Fun.thy | file | annotate | diff | comparison | revisions |
--- 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)