# HG changeset patch
# User Andreas Lochbihler
# Date 1423660559 -3600
# Node ID 76d7c593c6e85e9c3fb9876004657900cac03640
# Parent  2fb0c0fc62a319cc16cc7bd810502a1f4943b73b
add lema about card and vimage

diff -r 2fb0c0fc62a3 -r 76d7c593c6e8 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Wed Feb 11 14:12:30 2015 +0100
+++ b/src/HOL/Finite_Set.thy	Wed Feb 11 14:15:59 2015 +0100
@@ -1638,6 +1638,8 @@
 shows "finite A"
 using assms finite_imageD finite_subset by blast
 
+lemma card_vimage_inj: "\<lbrakk> inj f; A \<subseteq> range f \<rbrakk> \<Longrightarrow> card (f -` A) = card A"
+by(auto 4 3 simp add: subset_image_iff inj_vimage_image_eq intro: card_image[symmetric, OF subset_inj_on])
 
 subsubsection {* Pigeonhole Principles *}