src/HOL/Library/FuncSet.thy
changeset 14745 94be403deb84
parent 14706 71590b7733b7
child 14762 bd349ff7907a
     1.1 --- a/src/HOL/Library/FuncSet.thy	Fri May 14 16:49:12 2004 +0200
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Fri May 14 16:49:42 2004 +0200
     1.3 @@ -165,4 +165,17 @@
     1.4    apply (simp add: f_Inv_f)
     1.5    done
     1.6  
     1.7 +
     1.8 +subsection{*Cardinality*}
     1.9 +
    1.10 +lemma card_inj: "[|f \<in> A\<rightarrow>B; inj_on f A; finite B|] ==> card(A) \<le> card(B)"
    1.11 +apply (rule card_inj_on_le)
    1.12 +apply (auto simp add: Pi_def)
    1.13 +done
    1.14 +
    1.15 +lemma card_bij:
    1.16 +     "[|f \<in> A\<rightarrow>B; inj_on f A;
    1.17 +        g \<in> B\<rightarrow>A; inj_on g B; finite A; finite B|] ==> card(A) = card(B)"
    1.18 +by (blast intro: card_inj order_antisym)
    1.19 +
    1.20  end