equal
deleted
inserted
replaced
278 case insert then show ?case |
278 case insert then show ?case |
279 by (clarsimp simp del: image_insert simp add: image_insert [symmetric]) |
279 by (clarsimp simp del: image_insert simp add: image_insert [symmetric]) |
280 blast |
280 blast |
281 qed |
281 qed |
282 |
282 |
283 lemma finite_vimageI: |
283 lemma finite_vimage_IntI: |
284 "finite F \<Longrightarrow> inj h \<Longrightarrow> finite (h -` F)" |
284 "finite F \<Longrightarrow> inj_on h A \<Longrightarrow> finite (h -` F \<inter> A)" |
285 apply (induct rule: finite_induct) |
285 apply (induct rule: finite_induct) |
286 apply simp_all |
286 apply simp_all |
287 apply (subst vimage_insert) |
287 apply (subst vimage_insert) |
288 apply (simp add: finite_subset [OF inj_vimage_singleton]) |
288 apply (simp add: finite_subset [OF inj_on_vimage_singleton] Int_Un_distrib2) |
289 done |
289 done |
|
290 |
|
291 lemma finite_vimageI: |
|
292 "finite F \<Longrightarrow> inj h \<Longrightarrow> finite (h -` F)" |
|
293 using finite_vimage_IntI[of F h UNIV] by auto |
290 |
294 |
291 lemma finite_vimageD: |
295 lemma finite_vimageD: |
292 assumes fin: "finite (h -` F)" and surj: "surj h" |
296 assumes fin: "finite (h -` F)" and surj: "surj h" |
293 shows "finite F" |
297 shows "finite F" |
294 proof - |
298 proof - |