new lemma bij_comp
authornipkow
Mon Aug 10 17:00:41 2009 +0200 (2009-08-10)
changeset 323377887cb2848bb
parent 32336 e88b295aae35
child 32338 e73eb2db4727
child 32366 b269b56b6a14
new lemma bij_comp
src/HOL/Fun.thy
     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)