23 |
23 |
24 tot_ord_def "tot_ord(A,r) == part_ord(A,r) & linear(A,r)" |
24 tot_ord_def "tot_ord(A,r) == part_ord(A,r) & linear(A,r)" |
25 |
25 |
26 well_ord_def "well_ord(A,r) == tot_ord(A,r) & wf[A](r)" |
26 well_ord_def "well_ord(A,r) == tot_ord(A,r) & wf[A](r)" |
27 |
27 |
28 mono_map_def "mono_map(A,r,B,s) == \ |
28 mono_map_def "mono_map(A,r,B,s) == |
29 \ {f: A->B. ALL x:A. ALL y:A. <x,y>:r --> <f`x,f`y>:s}" |
29 {f: A->B. ALL x:A. ALL y:A. <x,y>:r --> <f`x,f`y>:s}" |
30 |
30 |
31 ord_iso_def "ord_iso(A,r,B,s) == \ |
31 ord_iso_def "ord_iso(A,r,B,s) == |
32 \ {f: bij(A,B). ALL x:A. ALL y:A. <x,y>:r <-> <f`x,f`y>:s}" |
32 {f: bij(A,B). ALL x:A. ALL y:A. <x,y>:r <-> <f`x,f`y>:s}" |
33 |
33 |
34 pred_def "pred(A,x,r) == {y:A. <y,x>:r}" |
34 pred_def "pred(A,x,r) == {y:A. <y,x>:r}" |
35 |
35 |
36 ord_iso_map_def |
36 ord_iso_map_def |
37 "ord_iso_map(A,r,B,s) == \ |
37 "ord_iso_map(A,r,B,s) == |
38 \ UN x:A. UN y:B. UN f: ord_iso(pred(A,x,r), r, pred(B,y,s), s). \ |
38 UN x:A. UN y:B. UN f: ord_iso(pred(A,x,r), r, pred(B,y,s), s). |
39 \ {<x,y>}" |
39 {<x,y>}" |
40 |
40 |
41 end |
41 end |