equal
deleted
inserted
replaced
25 |
25 |
26 defs |
26 defs |
27 |
27 |
28 monofun "monofun(f) == ! x y. x << y --> f(x) << f(y)" |
28 monofun "monofun(f) == ! x y. x << y --> f(x) << f(y)" |
29 |
29 |
30 contlub "contlub(f) == ! Y. is_chain(Y) --> |
30 contlub "contlub(f) == ! Y. chain(Y) --> |
31 f(lub(range(Y))) = lub(range(% i. f(Y(i))))" |
31 f(lub(range(Y))) = lub(range(% i. f(Y(i))))" |
32 |
32 |
33 cont "cont(f) == ! Y. is_chain(Y) --> |
33 cont "cont(f) == ! Y. chain(Y) --> |
34 range(% i. f(Y(i))) <<| f(lub(range(Y)))" |
34 range(% i. f(Y(i))) <<| f(lub(range(Y)))" |
35 |
35 |
36 (* ------------------------------------------------------------------------ *) |
36 (* ------------------------------------------------------------------------ *) |
37 (* the main purpose of cont.thy is to show: *) |
37 (* the main purpose of cont.thy is to show: *) |
38 (* monofun(f) & contlub(f) <==> cont(f) *) |
38 (* monofun(f) & contlub(f) <==> cont(f) *) |