src/HOL/Fun.thy
changeset 57282 7da3e398804c
parent 56608 8e3c848008fa
child 58111 82db9ad610b9
     1.1 --- a/src/HOL/Fun.thy	Fri Jun 20 09:55:31 2014 +0200
     1.2 +++ b/src/HOL/Fun.thy	Sat Jun 21 10:41:02 2014 +0200
     1.3 @@ -295,6 +295,13 @@
     1.4  apply (drule_tac x = x in spec, blast)
     1.5  done
     1.6  
     1.7 +lemma bij_betw_imageI:
     1.8 +  "\<lbrakk> inj_on f A; f ` A = B \<rbrakk> \<Longrightarrow> bij_betw f A B"
     1.9 +unfolding bij_betw_def by clarify
    1.10 +
    1.11 +lemma bij_betw_imp_surj_on: "bij_betw f A B \<Longrightarrow> f ` A = B"
    1.12 +  unfolding bij_betw_def by clarify
    1.13 +
    1.14  lemma bij_betw_imp_surj: "bij_betw f A UNIV \<Longrightarrow> surj f"
    1.15    unfolding bij_betw_def by auto
    1.16