src/HOL/Fun.thy
changeset 32337 7887cb2848bb
parent 32139 e271a64f03ff
child 32554 4ccd84fb19d3
     1.1 --- a/src/HOL/Fun.thy	Sat Aug 08 11:40:22 2009 +0200
     1.2 +++ b/src/HOL/Fun.thy	Mon Aug 10 17:00:41 2009 +0200
     1.3 @@ -250,6 +250,9 @@
     1.4  lemma bij_betw_imp_inj_on: "bij_betw f A B \<Longrightarrow> inj_on f A"
     1.5  by (simp add: bij_betw_def)
     1.6  
     1.7 +lemma bij_comp: "bij f \<Longrightarrow> bij g \<Longrightarrow> bij (g o f)"
     1.8 +by(fastsimp intro: comp_inj_on comp_surj simp: bij_def surj_range)
     1.9 +
    1.10  lemma bij_betw_trans:
    1.11    "bij_betw f A B \<Longrightarrow> bij_betw g B C \<Longrightarrow> bij_betw (g o f) A C"
    1.12  by(auto simp add:bij_betw_def comp_inj_on)