src/HOL/Fun.thy
changeset 31438 a1c4c1500abe
parent 31202 52d332f8f909
child 31604 eb2f9d709296
     1.1 --- a/src/HOL/Fun.thy	Wed Jun 03 12:24:09 2009 -0700
     1.2 +++ b/src/HOL/Fun.thy	Thu Jun 04 13:26:32 2009 +0200
     1.3 @@ -250,6 +250,10 @@
     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_betw_trans:
     1.8 +  "bij_betw f A B \<Longrightarrow> bij_betw g B C \<Longrightarrow> bij_betw (g o f) A C"
     1.9 +by(auto simp add:bij_betw_def comp_inj_on)
    1.10 +
    1.11  lemma bij_betw_inv: assumes "bij_betw f A B" shows "EX g. bij_betw g B A"
    1.12  proof -
    1.13    have i: "inj_on f A" and s: "f ` A = B"
    1.14 @@ -300,6 +304,9 @@
    1.15  apply (blast del: subsetI intro: vimage_subsetI vimage_subsetD)
    1.16  done
    1.17  
    1.18 +lemma inj_on_Un_image_eq_iff: "inj_on f (A \<union> B) \<Longrightarrow> f ` A = f ` B \<longleftrightarrow> A = B"
    1.19 +by(blast dest: inj_onD)
    1.20 +
    1.21  lemma inj_on_image_Int:
    1.22     "[| inj_on f C;  A<=C;  B<=C |] ==> f`(A Int B) = f`A Int f`B"
    1.23  apply (simp add: inj_on_def, blast)