summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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