src/HOL/Fun.thy
changeset 41657 89451110ba8e
parent 41505 6d19301074cf
child 42238 d53dccb38dd1
     1.1 --- a/src/HOL/Fun.thy	Fri Jan 21 09:41:59 2011 +0100
     1.2 +++ b/src/HOL/Fun.thy	Fri Jan 21 09:44:12 2011 +0100
     1.3 @@ -546,12 +546,20 @@
     1.4  apply (simp_all (no_asm_simp) add: inj_image_Compl_subset surj_Compl_image_subset)
     1.5  done
     1.6  
     1.7 +lemma inj_vimage_singleton: "inj f \<Longrightarrow> f -` {a} \<subseteq> {THE x. f x = a}"
     1.8 +  -- {* The inverse image of a singleton under an injective function
     1.9 +         is included in a singleton. *}
    1.10 +  apply (auto simp add: inj_on_def)
    1.11 +  apply (blast intro: the_equality [symmetric])
    1.12 +  done
    1.13 +
    1.14  lemma (in ordered_ab_group_add) inj_uminus[simp, intro]: "inj_on uminus A"
    1.15    by (auto intro!: inj_onI)
    1.16  
    1.17  lemma (in linorder) strict_mono_imp_inj_on: "strict_mono f \<Longrightarrow> inj_on f A"
    1.18    by (auto intro!: inj_onI dest: strict_mono_eq)
    1.19  
    1.20 +
    1.21  subsection{*Function Updating*}
    1.22  
    1.23  definition