src/HOL/Finite_Set.thy
changeset 43991 f4a7697011c5
parent 43866 8a50dc70cbff
child 44744 bdf8eb8f126b
child 44831 4ea848959340
     1.1 --- a/src/HOL/Finite_Set.thy	Tue Jul 26 22:53:06 2011 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Wed Jul 27 19:34:30 2011 +0200
     1.3 @@ -280,14 +280,18 @@
     1.4         blast
     1.5  qed
     1.6  
     1.7 -lemma finite_vimageI:
     1.8 -  "finite F \<Longrightarrow> inj h \<Longrightarrow> finite (h -` F)"
     1.9 +lemma finite_vimage_IntI:
    1.10 +  "finite F \<Longrightarrow> inj_on h A \<Longrightarrow> finite (h -` F \<inter> A)"
    1.11    apply (induct rule: finite_induct)
    1.12     apply simp_all
    1.13    apply (subst vimage_insert)
    1.14 -  apply (simp add: finite_subset [OF inj_vimage_singleton])
    1.15 +  apply (simp add: finite_subset [OF inj_on_vimage_singleton] Int_Un_distrib2)
    1.16    done
    1.17  
    1.18 +lemma finite_vimageI:
    1.19 +  "finite F \<Longrightarrow> inj h \<Longrightarrow> finite (h -` F)"
    1.20 +  using finite_vimage_IntI[of F h UNIV] by auto
    1.21 +
    1.22  lemma finite_vimageD:
    1.23    assumes fin: "finite (h -` F)" and surj: "surj h"
    1.24    shows "finite F"