src/HOL/Fun.thy
changeset 15439 71c0f98e31f1
parent 15303 eedbb8d22ca2
child 15510 9de204d7b699
     1.1 --- a/src/HOL/Fun.thy	Thu Jan 13 14:56:37 2005 +0100
     1.2 +++ b/src/HOL/Fun.thy	Fri Jan 14 12:00:27 2005 +0100
     1.3 @@ -163,6 +163,12 @@
     1.4  apply blast
     1.5  done
     1.6  
     1.7 +lemma inj_on_image_iff: "\<lbrakk> ALL x:A. ALL y:A. (g(f x) = g(f y)) = (g x = g y);
     1.8 +  inj_on f A \<rbrakk> \<Longrightarrow> inj_on g (f ` A) = inj_on g A"
     1.9 +apply(unfold inj_on_def)
    1.10 +apply blast
    1.11 +done
    1.12 +
    1.13  lemma inj_on_contraD: "[| inj_on f A;  ~x=y;  x:A;  y:A |] ==> ~ f(x)=f(y)"
    1.14  by (unfold inj_on_def, blast)
    1.15