# HG changeset patch
# User nipkow
# Date 1249916441 -7200
# Node ID 7887cb2848bbe6b73fc8489e68601a1c25a9f040
# Parent  e88b295aae351f732d56b51105b347d7dfc0d8d5
new lemma bij_comp

diff -r e88b295aae35 -r 7887cb2848bb src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Sat Aug 08 11:40:22 2009 +0200
+++ b/src/HOL/Fun.thy	Mon Aug 10 17:00:41 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)