167 then have "eventually (\<lambda>x. y < X x) F" |
167 then have "eventually (\<lambda>x. y < X x) F" |
168 by (auto elim!: eventually_elim1 dest: less_INF_D) } |
168 by (auto elim!: eventually_elim1 dest: less_INF_D) } |
169 moreover |
169 moreover |
170 { fix y P assume "y < C" and y: "\<forall>y<C. eventually (\<lambda>x. y < X x) F" |
170 { fix y P assume "y < C" and y: "\<forall>y<C. eventually (\<lambda>x. y < X x) F" |
171 have "\<exists>P. eventually P F \<and> y < INFI (Collect P) X" |
171 have "\<exists>P. eventually P F \<and> y < INFI (Collect P) X" |
172 proof cases |
172 proof (cases "\<exists>z. y < z \<and> z < C") |
173 assume "\<exists>z. y < z \<and> z < C" |
173 case True |
174 then guess z .. note z = this |
174 then obtain z where z: "y < z \<and> z < C" .. |
175 moreover from z have "z \<le> INFI {x. z < X x} X" |
175 moreover from z have "z \<le> INFI {x. z < X x} X" |
176 by (auto intro!: INF_greatest) |
176 by (auto intro!: INF_greatest) |
177 ultimately show ?thesis |
177 ultimately show ?thesis |
178 using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto |
178 using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto |
179 next |
179 next |
180 assume "\<not> (\<exists>z. y < z \<and> z < C)" |
180 case False |
181 then have "C \<le> INFI {x. y < X x} X" |
181 then have "C \<le> INFI {x. y < X x} X" |
182 by (intro INF_greatest) auto |
182 by (intro INF_greatest) auto |
183 with `y < C` show ?thesis |
183 with `y < C` show ?thesis |
184 using y by (intro exI[of _ "\<lambda>x. y < X x"]) auto |
184 using y by (intro exI[of _ "\<lambda>x. y < X x"]) auto |
185 qed } |
185 qed } |
238 then show "f0 \<le> SUPR (Collect P) f" |
238 then show "f0 \<le> SUPR (Collect P) f" |
239 by (rule tendsto_le[OF ntriv tendsto_const lim]) |
239 by (rule tendsto_le[OF ntriv tendsto_const lim]) |
240 next |
240 next |
241 fix y assume lower: "\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f" |
241 fix y assume lower: "\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f" |
242 show "y \<le> f0" |
242 show "y \<le> f0" |
243 proof cases |
243 proof (cases "\<exists>z. f0 < z \<and> z < y") |
244 assume "\<exists>z. f0 < z \<and> z < y" |
244 case True |
245 then guess z .. |
245 then obtain z where "f0 < z \<and> z < y" .. |
246 moreover have "SUPR {x. f x < z} f \<le> z" |
246 moreover have "SUPR {x. f x < z} f \<le> z" |
247 by (rule SUP_least) simp |
247 by (rule SUP_least) simp |
248 ultimately show ?thesis |
248 ultimately show ?thesis |
249 using lim[THEN topological_tendstoD, THEN lower, of "{..< z}"] by auto |
249 using lim[THEN topological_tendstoD, THEN lower, of "{..< z}"] by auto |
250 next |
250 next |
251 assume discrete: "\<not> (\<exists>z. f0 < z \<and> z < y)" |
251 case False |
252 show ?thesis |
252 show ?thesis |
253 proof (rule classical) |
253 proof (rule classical) |
254 assume "\<not> y \<le> f0" |
254 assume "\<not> y \<le> f0" |
255 then have "eventually (\<lambda>x. f x < y) F" |
255 then have "eventually (\<lambda>x. f x < y) F" |
256 using lim[THEN topological_tendstoD, of "{..< y}"] by auto |
256 using lim[THEN topological_tendstoD, of "{..< y}"] by auto |
257 then have "eventually (\<lambda>x. f x \<le> f0) F" |
257 then have "eventually (\<lambda>x. f x \<le> f0) F" |
258 using discrete by (auto elim!: eventually_elim1 simp: not_less) |
258 using False by (auto elim!: eventually_elim1 simp: not_less) |
259 then have "y \<le> SUPR {x. f x \<le> f0} f" |
259 then have "y \<le> SUPR {x. f x \<le> f0} f" |
260 by (rule lower) |
260 by (rule lower) |
261 moreover have "SUPR {x. f x \<le> f0} f \<le> f0" |
261 moreover have "SUPR {x. f x \<le> f0} f \<le> f0" |
262 by (intro SUP_least) simp |
262 by (intro SUP_least) simp |
263 ultimately show "y \<le> f0" by simp |
263 ultimately show "y \<le> f0" by simp |