bij <--> bij_betw
authorhoelzl
Thu Sep 02 10:36:45 2010 +0200 (2010-09-02)
changeset 39074211e4f6aad63
parent 39073 8520a1f89db1
child 39075 a18e5946d63c
bij <--> bij_betw
src/HOL/Fun.thy
     1.1 --- a/src/HOL/Fun.thy	Thu Sep 02 10:18:15 2010 +0200
     1.2 +++ b/src/HOL/Fun.thy	Thu Sep 02 10:36:45 2010 +0200
     1.3 @@ -262,6 +262,15 @@
     1.4  apply (drule_tac x = x in spec, blast)
     1.5  done
     1.6  
     1.7 +lemma surj_range_iff: "surj f \<longleftrightarrow> range f = UNIV"
     1.8 +  unfolding expand_set_eq image_iff surj_def by auto
     1.9 +
    1.10 +lemma bij_betw_imp_surj: "bij_betw f A UNIV \<Longrightarrow> surj f"
    1.11 +  unfolding bij_betw_def surj_range_iff by auto
    1.12 +
    1.13 +lemma bij_eq_bij_betw: "bij f \<longleftrightarrow> bij_betw f UNIV UNIV"
    1.14 +  unfolding bij_def surj_range_iff bij_betw_def ..
    1.15 +
    1.16  lemma bijI: "[| inj f; surj f |] ==> bij f"
    1.17  by (simp add: bij_def)
    1.18