src/ZF/Perm.thy
changeset 13513 b9e14471629c
parent 13357 6f54e992777e
child 13611 2edf034c902a
equal deleted inserted replaced
13512:80edb859fd24 13513:b9e14471629c
    95     "[| <a,b>:f;  <c,b>:f;  f: inj(A,B) |] ==> a=c"
    95     "[| <a,b>:f;  <c,b>:f;  f: inj(A,B) |] ==> a=c"
    96 apply (unfold inj_def)
    96 apply (unfold inj_def)
    97 apply (blast dest: Pair_mem_PiD)
    97 apply (blast dest: Pair_mem_PiD)
    98 done
    98 done
    99 
    99 
   100 lemma inj_apply_equality: "[| f:inj(A,B);  a:A;  b:A;  f`a=f`b |] ==> a=b"
   100 lemma inj_apply_equality: "[| f:inj(A,B);  f`a=f`b;  a:A;  b:A |] ==> a=b"
   101 by (unfold inj_def, blast)
   101 by (unfold inj_def, blast)
       
   102 
   102 
   103 
   103 (** A function with a left inverse is an injection **)
   104 (** A function with a left inverse is an injection **)
   104 
   105 
   105 lemma f_imp_injective: "[| f: A->B;  ALL x:A. d(f`x)=x |] ==> f: inj(A,B)"
   106 lemma f_imp_injective: "[| f: A->B;  ALL x:A. d(f`x)=x |] ==> f: inj(A,B)"
   106 apply (simp (no_asm_simp) add: inj_def)
   107 apply (simp (no_asm_simp) add: inj_def)