# HG changeset patch
# User paulson
# Date 1084546182 -7200
# Node ID 94be403deb84a2e9fe902da8ccc9b4e19bab0e91
# Parent  7ccfc167e451fca1ee96a2f270b0138c1cba2803
new lemmas

diff -r 7ccfc167e451 -r 94be403deb84 src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Fri May 14 16:49:12 2004 +0200
+++ b/src/HOL/Library/FuncSet.thy	Fri May 14 16:49:42 2004 +0200
@@ -165,4 +165,17 @@
   apply (simp add: f_Inv_f)
   done
 
+
+subsection{*Cardinality*}
+
+lemma card_inj: "[|f \<in> A\<rightarrow>B; inj_on f A; finite B|] ==> card(A) \<le> card(B)"
+apply (rule card_inj_on_le)
+apply (auto simp add: Pi_def)
+done
+
+lemma card_bij:
+     "[|f \<in> A\<rightarrow>B; inj_on f A;
+        g \<in> B\<rightarrow>A; inj_on g B; finite A; finite B|] ==> card(A) = card(B)"
+by (blast intro: card_inj order_antisym)
+
 end