src/HOL/Fun.thy
changeset 43991 f4a7697011c5
parent 43874 74f1f2dd8f52
child 44277 bcb696533579
     1.1 --- a/src/HOL/Fun.thy	Tue Jul 26 22:53:06 2011 +0200
     1.2 +++ b/src/HOL/Fun.thy	Wed Jul 27 19:34:30 2011 +0200
     1.3 @@ -556,6 +556,10 @@
     1.4    apply (blast intro: the_equality [symmetric])
     1.5    done
     1.6  
     1.7 +lemma inj_on_vimage_singleton:
     1.8 +  "inj_on f A \<Longrightarrow> f -` {a} \<inter> A \<subseteq> {THE x. x \<in> A \<and> f x = a}"
     1.9 +  by (auto simp add: inj_on_def intro: the_equality [symmetric])
    1.10 +
    1.11  lemma (in ordered_ab_group_add) inj_uminus[simp, intro]: "inj_on uminus A"
    1.12    by (auto intro!: inj_onI)
    1.13