73 "\<lbrakk>monofun f; range Y <| u\<rbrakk> \<Longrightarrow> range (\<lambda>i. f (Y i)) <| f u" |
73 "\<lbrakk>monofun f; range Y <| u\<rbrakk> \<Longrightarrow> range (\<lambda>i. f (Y i)) <| f u" |
74 apply (rule ub_rangeI) |
74 apply (rule ub_rangeI) |
75 apply (erule monofunE) |
75 apply (erule monofunE) |
76 apply (erule ub_rangeD) |
76 apply (erule ub_rangeD) |
77 done |
77 done |
78 |
|
79 lemma ub2ub_monofun': |
|
80 "\<lbrakk>monofun f; S <| u\<rbrakk> \<Longrightarrow> f ` S <| f u" |
|
81 apply (rule ub_imageI) |
|
82 apply (erule monofunE) |
|
83 apply (erule (1) is_ubD) |
|
84 done |
|
85 |
|
86 text {* monotone functions map directed sets to directed sets *} |
|
87 |
|
88 lemma dir2dir_monofun: |
|
89 assumes f: "monofun f" |
|
90 assumes S: "directed S" |
|
91 shows "directed (f ` S)" |
|
92 proof (rule directedI) |
|
93 from directedD1 [OF S] |
|
94 obtain x where "x \<in> S" .. |
|
95 hence "f x \<in> f ` S" by simp |
|
96 thus "\<exists>x. x \<in> f ` S" .. |
|
97 next |
|
98 fix x assume "x \<in> f ` S" |
|
99 then obtain a where x: "x = f a" and a: "a \<in> S" .. |
|
100 fix y assume "y \<in> f ` S" |
|
101 then obtain b where y: "y = f b" and b: "b \<in> S" .. |
|
102 from directedD2 [OF S a b] |
|
103 obtain c where "c \<in> S" and "a \<sqsubseteq> c \<and> b \<sqsubseteq> c" .. |
|
104 hence "f c \<in> f ` S" and "x \<sqsubseteq> f c \<and> y \<sqsubseteq> f c" |
|
105 using monofunE [OF f] x y by simp_all |
|
106 thus "\<exists>z\<in>f ` S. x \<sqsubseteq> z \<and> y \<sqsubseteq> z" .. |
|
107 qed |
|
108 |
78 |
109 text {* left to right: @{prop "monofun f \<and> contlub f \<Longrightarrow> cont f"} *} |
79 text {* left to right: @{prop "monofun f \<and> contlub f \<Longrightarrow> cont f"} *} |
110 |
80 |
111 lemma monocontlub2cont: "\<lbrakk>monofun f; contlub f\<rbrakk> \<Longrightarrow> cont f" |
81 lemma monocontlub2cont: "\<lbrakk>monofun f; contlub f\<rbrakk> \<Longrightarrow> cont f" |
112 apply (rule contI) |
82 apply (rule contI) |