src/HOL/Finite_Set.thy

--- a/src/HOL/Finite_Set.thy	Sun Mar 13 14:42:07 2016 +0100
+++ b/src/HOL/Finite_Set.thy	Mon Mar 14 14:19:06 2016 +0000
@@ -291,6 +291,11 @@
   then show "finite A" by simp
 qed
 
+lemma finite_image_iff:
+  assumes "inj_on f A"
+  shows "finite (f ` A) \<longleftrightarrow> finite A"
+using assms finite_imageD by blast
+
 lemma finite_surj:
   "finite A \<Longrightarrow> B \<subseteq> f ` A \<Longrightarrow> finite B"
   by (erule finite_subset) (rule finite_imageI)