src/HOL/Fun.thy
changeset 42903 ec9eb1fbfcb8
parent 42238 d53dccb38dd1
child 43705 8e421a529a48
equal deleted inserted replaced
42902:e8dbf90a2f3b 42903:ec9eb1fbfcb8
   476 by(unfold bij_betw_def inj_on_def, auto simp add: inj_on_def)
   476 by(unfold bij_betw_def inj_on_def, auto simp add: inj_on_def)
   477 
   477 
   478 lemma surj_image_vimage_eq: "surj f ==> f ` (f -` A) = A"
   478 lemma surj_image_vimage_eq: "surj f ==> f ` (f -` A) = A"
   479 by simp
   479 by simp
   480 
   480 
       
   481 lemma surj_vimage_empty:
       
   482   assumes "surj f" shows "f -` A = {} \<longleftrightarrow> A = {}"
       
   483   using surj_image_vimage_eq[OF `surj f`, of A]
       
   484   by (intro iffI) fastsimp+
       
   485 
   481 lemma inj_vimage_image_eq: "inj f ==> f -` (f ` A) = A"
   486 lemma inj_vimage_image_eq: "inj f ==> f -` (f ` A) = A"
   482 by (simp add: inj_on_def, blast)
   487 by (simp add: inj_on_def, blast)
   483 
   488 
   484 lemma vimage_subsetD: "surj f ==> f -` B <= A ==> B <= f ` A"
   489 lemma vimage_subsetD: "surj f ==> f -` B <= A ==> B <= f ` A"
   485 by (blast intro: sym)
   490 by (blast intro: sym)