--- a/src/ZF/Order.thy Wed Dec 14 16:51:16 1994 +0100
+++ b/src/ZF/Order.thy Wed Dec 14 16:54:13 1994 +0100
@@ -11,8 +11,10 @@
part_ord :: "[i,i]=>o" (*Strict partial ordering*)
linear, tot_ord :: "[i,i]=>o" (*Strict total ordering*)
well_ord :: "[i,i]=>o" (*Well-ordering*)
+ mono_map :: "[i,i,i,i]=>i" (*Order-preserving maps*)
ord_iso :: "[i,i,i,i]=>i" (*Order isomorphisms*)
pred :: "[i,i,i]=>i" (*Set of predecessors*)
+ ord_iso_map :: "[i,i,i,i]=>i" (*Construction for linearity theorem*)
defs
part_ord_def "part_ord(A,r) == irrefl(A,r) & trans[A](r)"
@@ -23,9 +25,17 @@
well_ord_def "well_ord(A,r) == tot_ord(A,r) & wf[A](r)"
+ mono_map_def "mono_map(A,r,B,s) == \
+\ {f: A->B. ALL x:A. ALL y:A. <x,y>:r --> <f`x,f`y>:s}"
+
ord_iso_def "ord_iso(A,r,B,s) == \
\ {f: bij(A,B). ALL x:A. ALL y:A. <x,y>:r <-> <f`x,f`y>:s}"
pred_def "pred(A,x,r) == {y:A. <y,x>:r}"
+ ord_iso_map_def
+ "ord_iso_map(A,r,B,s) == \
+\ UN x:A. UN y:B. UN f: ord_iso(pred(A,x,r), r, pred(B,y,s), s). \
+\ {<x,y>}"
+
end