src/HOL/Finite_Set.thy

 lemma card_bij_eq:
   "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
      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 *}
 
 lemma pigeonhole: "card A > card(f ` A) \<Longrightarrow> ~ inj_on f A "
 by (auto dest: card_image less_irrefl_nat)