# HG changeset patch # User hoelzl # Date 1283416605 -7200 # Node ID 211e4f6aad6397983968f827bd0765c74fd9ba72 # Parent 8520a1f89db12ae8d35dda82038e9e7db6c9aa76 bij <--> bij_betw diff -r 8520a1f89db1 -r 211e4f6aad63 src/HOL/Fun.thy --- a/src/HOL/Fun.thy Thu Sep 02 10:18:15 2010 +0200 +++ b/src/HOL/Fun.thy Thu Sep 02 10:36:45 2010 +0200 @@ -262,6 +262,15 @@ apply (drule_tac x = x in spec, blast) done +lemma surj_range_iff: "surj f \ range f = UNIV" + unfolding expand_set_eq image_iff surj_def by auto + +lemma bij_betw_imp_surj: "bij_betw f A UNIV \ surj f" + unfolding bij_betw_def surj_range_iff by auto + +lemma bij_eq_bij_betw: "bij f \ bij_betw f UNIV UNIV" + unfolding bij_def surj_range_iff bij_betw_def .. + lemma bijI: "[| inj f; surj f |] ==> bij f" by (simp add: bij_def)