--- a/src/ZF/Constructible/Wellorderings.thy Wed Aug 21 15:57:08 2002 +0200
+++ b/src/ZF/Constructible/Wellorderings.thy Wed Aug 21 15:57:24 2002 +0200
@@ -42,7 +42,7 @@
--> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & <z,y> \<in> r))"
wellordered :: "[i=>o,i,i]=>o"
- --{*every non-empty subset of @{text A} has an @{text r}-minimal element*}
+ --{*linear and wellfounded on @{text A}*}
"wellordered(M,A,r) ==
transitive_rel(M,A,r) & linear_rel(M,A,r) & wellfounded_on(M,A,r)"
--- a/src/ZF/Perm.thy Wed Aug 21 15:57:08 2002 +0200
+++ b/src/ZF/Perm.thy Wed Aug 21 15:57:24 2002 +0200
@@ -97,9 +97,10 @@
apply (blast dest: Pair_mem_PiD)
done
-lemma inj_apply_equality: "[| f:inj(A,B); a:A; b:A; f`a=f`b |] ==> a=b"
+lemma inj_apply_equality: "[| f:inj(A,B); f`a=f`b; a:A; b:A |] ==> a=b"
by (unfold inj_def, blast)
+
(** A function with a left inverse is an injection **)
lemma f_imp_injective: "[| f: A->B; ALL x:A. d(f`x)=x |] ==> f: inj(A,B)"