# HG changeset patch
# User lcp
# Date 787420453 -3600
# Node ID 2a871417e7fc4f623828f38b56fc1d08f504fed2
# Parent  c2ef808dc93898f0ccbef6ac0c3e7d6e18657a34
added constants mono_map, ord_iso_map

diff -r c2ef808dc938 -r 2a871417e7fc src/ZF/Order.thy
--- 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