# HG changeset patch
# User haftmann
# Date 1245749487 -7200
# Node ID 159cd6b5e5d4cc82f15057f43d6f65efdc0128fe
# Parent  530596c997da92bb322b204b37ba8e369ae458b8
lemma finite_image_set by Jeremy Avigad

diff -r 530596c997da -r 159cd6b5e5d4 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Mon Jun 22 14:25:22 2009 +0200
+++ b/src/HOL/Finite_Set.thy	Tue Jun 23 11:31:27 2009 +0200
@@ -285,6 +285,10 @@
   -- {* The image of a finite set is finite. *}
   by (induct set: finite) simp_all
 
+lemma finite_image_set [simp]:
+  "finite {x. P x} \<Longrightarrow> finite { f x | x. P x }"
+  by (simp add: image_Collect [symmetric])
+
 lemma finite_surj: "finite A ==> B <= f ` A ==> finite B"
   apply (frule finite_imageI)
   apply (erule finite_subset, assumption)