merged
authorhaftmann
Tue, 11 Aug 2009 10:05:53 +0200
changeset 32357 84a6d701e36f
parent 32338 e73eb2db4727 (diff)
parent 32356 e11cd88e6ade (current diff)
child 32358 98c00ee9e786
merged
--- a/src/HOL/Fun.thy	Tue Aug 11 10:05:16 2009 +0200
+++ b/src/HOL/Fun.thy	Tue Aug 11 10:05:53 2009 +0200
@@ -250,6 +250,9 @@
 lemma bij_betw_imp_inj_on: "bij_betw f A B \<Longrightarrow> inj_on f A"
 by (simp add: bij_betw_def)
 
+lemma bij_comp: "bij f \<Longrightarrow> bij g \<Longrightarrow> bij (g o f)"
+by(fastsimp intro: comp_inj_on comp_surj simp: bij_def surj_range)
+
 lemma bij_betw_trans:
   "bij_betw f A B \<Longrightarrow> bij_betw g B C \<Longrightarrow> bij_betw (g o f) A C"
 by(auto simp add:bij_betw_def comp_inj_on)
--- a/src/HOL/Library/Nat_Int_Bij.thy	Tue Aug 11 10:05:16 2009 +0200
+++ b/src/HOL/Library/Nat_Int_Bij.thy	Tue Aug 11 10:05:53 2009 +0200
@@ -165,5 +165,11 @@
 lemma inj_int_to_nat_bij: "inj int_to_nat_bij"
 by(simp add:inv_nat_to_int_bij[symmetric] surj_nat_to_int_bij surj_imp_inj_inv)
 
+lemma bij_nat_to_int_bij: "bij nat_to_int_bij"
+by(simp add:bij_def inj_nat_to_int_bij surj_nat_to_int_bij)
+
+lemma bij_int_to_nat_bij: "bij int_to_nat_bij"
+by(simp add:bij_def inj_int_to_nat_bij surj_int_to_nat_bij)
+
 
 end