src/ZF/Perm.thy
 changeset 13513 b9e14471629c parent 13357 6f54e992777e child 13611 2edf034c902a
equal 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)`