inj_comp and inj_fun
authorhaftmann
Fri Aug 20 17:46:55 2010 +0200 (2010-08-20)
changeset 38620b40524b74f77
parent 38619 25e401d53900
child 38621 d6cb7e625d75
inj_comp and inj_fun
src/HOL/Fun.thy
     1.1 --- a/src/HOL/Fun.thy	Fri Aug 20 08:52:01 2010 +0200
     1.2 +++ b/src/HOL/Fun.thy	Fri Aug 20 17:46:55 2010 +0200
     1.3 @@ -162,6 +162,13 @@
     1.4  lemma inj_on_eq_iff: "inj_on f A ==> x:A ==> y:A ==> (f(x) = f(y)) = (x=y)"
     1.5  by (force simp add: inj_on_def)
     1.6  
     1.7 +lemma inj_comp:
     1.8 +  "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (f \<circ> g)"
     1.9 +  by (simp add: inj_on_def)
    1.10 +
    1.11 +lemma inj_fun: "inj f \<Longrightarrow> inj (\<lambda>x y. f x)"
    1.12 +  by (simp add: inj_on_def expand_fun_eq)
    1.13 +
    1.14  lemma inj_eq: "inj f ==> (f(x) = f(y)) = (x=y)"
    1.15  by (simp add: inj_on_eq_iff)
    1.16