Two basic lemmas on bij_betw.
authorballarin
Sat Jun 21 10:41:02 2014 +0200 (2014-06-21)
changeset 572827da3e398804c
parent 57281 bb671e6b740d
child 57283 1f133cd8d3eb
Two basic lemmas on bij_betw.
src/HOL/Fun.thy
     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