src/HOL/Finite_Set.thy

--- a/src/HOL/Finite_Set.thy	Mon Nov 22 10:34:33 2010 +0100
+++ b/src/HOL/Finite_Set.thy	Tue Nov 23 14:14:17 2010 +0100
@@ -2179,6 +2179,11 @@
      finite A; finite B |] ==> card A = card B"
 by (auto intro: le_antisym card_inj_on_le)
 
+lemma bij_betw_finite:
+  assumes "bij_betw f A B"
+  shows "finite A \<longleftrightarrow> finite B"
+using assms unfolding bij_betw_def
+using finite_imageD[of f A] by auto
 
 subsubsection {* Pigeonhole Principles *}