# HG changeset patch
# User ballarin
# Date 1403340062 -7200
# Node ID 7da3e398804c2412e832c99193fd19e0909da7f6
# Parent  bb671e6b740dcd4b74e24593202079c609a165f2
Two basic lemmas on bij_betw.

diff -r bb671e6b740d -r 7da3e398804c src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Fri Jun 20 09:55:31 2014 +0200
+++ b/src/HOL/Fun.thy	Sat Jun 21 10:41:02 2014 +0200
@@ -295,6 +295,13 @@
 apply (drule_tac x = x in spec, blast)
 done
 
+lemma bij_betw_imageI:
+  "\<lbrakk> inj_on f A; f ` A = B \<rbrakk> \<Longrightarrow> bij_betw f A B"
+unfolding bij_betw_def by clarify
+
+lemma bij_betw_imp_surj_on: "bij_betw f A B \<Longrightarrow> f ` A = B"
+  unfolding bij_betw_def by clarify
+
 lemma bij_betw_imp_surj: "bij_betw f A UNIV \<Longrightarrow> surj f"
   unfolding bij_betw_def by auto