src/HOL/Fun.thy
changeset 58195 1fee63e0377d
parent 58111 82db9ad610b9
child 58839 ccda99401bc8
     1.1 --- a/src/HOL/Fun.thy	Fri Sep 05 16:09:03 2014 +0100
     1.2 +++ b/src/HOL/Fun.thy	Sat Sep 06 20:12:32 2014 +0200
     1.3 @@ -422,6 +422,17 @@
     1.4  using assms
     1.5  by(unfold bij_betw_def inj_on_def, auto simp add: inj_on_def)
     1.6  
     1.7 +lemma bij_pointE:
     1.8 +  assumes "bij f"
     1.9 +  obtains x where "y = f x" and "\<And>x'. y = f x' \<Longrightarrow> x' = x"
    1.10 +proof -
    1.11 +  from assms have "inj f" by (rule bij_is_inj)
    1.12 +  moreover from assms have "surj f" by (rule bij_is_surj)
    1.13 +  then have "y \<in> range f" by simp
    1.14 +  ultimately have "\<exists>!x. y = f x" by (simp add: range_ex1_eq)
    1.15 +  with that show thesis by blast
    1.16 +qed
    1.17 +
    1.18  lemma surj_image_vimage_eq: "surj f ==> f ` (f -` A) = A"
    1.19  by simp
    1.20