1335 shows "\<exists>x\<in>X. x < Inf X + e" |
1335 shows "\<exists>x\<in>X. x < Inf X + e" |
1336 proof (rule Inf_less_iff[THEN iffD1]) |
1336 proof (rule Inf_less_iff[THEN iffD1]) |
1337 show "Inf X < Inf X + e" using assms |
1337 show "Inf X < Inf X + e" using assms |
1338 by (cases e) auto |
1338 by (cases e) auto |
1339 qed |
1339 qed |
1340 |
|
1341 lemma (in complete_linorder) Sup_eq_top_iff: -- "FIXME move" |
|
1342 "Sup A = top \<longleftrightarrow> (\<forall>x<top. \<exists>i\<in>A. x < i)" |
|
1343 proof |
|
1344 assume *: "Sup A = top" |
|
1345 show "(\<forall>x<top. \<exists>i\<in>A. x < i)" unfolding * [symmetric] |
|
1346 proof (intro allI impI) |
|
1347 fix x assume "x < Sup A" then show "\<exists>i\<in>A. x < i" |
|
1348 unfolding less_Sup_iff by auto |
|
1349 qed |
|
1350 next |
|
1351 assume *: "\<forall>x<top. \<exists>i\<in>A. x < i" |
|
1352 show "Sup A = top" |
|
1353 proof (rule ccontr) |
|
1354 assume "Sup A \<noteq> top" |
|
1355 with top_greatest [of "Sup A"] |
|
1356 have "Sup A < top" unfolding le_less by auto |
|
1357 then have "Sup A < Sup A" |
|
1358 using * unfolding less_Sup_iff by auto |
|
1359 then show False by auto |
|
1360 qed |
|
1361 qed |
|
1362 |
|
1363 lemma (in complete_linorder) SUP_eq_top_iff: -- "FIXME move" |
|
1364 fixes f :: "'b \<Rightarrow> 'a" |
|
1365 shows "(SUP i:A. f i) = top \<longleftrightarrow> (\<forall>x<top. \<exists>i\<in>A. x < f i)" |
|
1366 unfolding SUPR_def Sup_eq_top_iff by auto |
|
1367 |
1340 |
1368 lemma SUP_nat_Infty: "(SUP i::nat. ereal (real i)) = \<infinity>" |
1341 lemma SUP_nat_Infty: "(SUP i::nat. ereal (real i)) = \<infinity>" |
1369 proof - |
1342 proof - |
1370 { fix x ::ereal assume "x \<noteq> \<infinity>" |
1343 { fix x ::ereal assume "x \<noteq> \<infinity>" |
1371 then have "\<exists>k::nat. x < ereal (real k)" |
1344 then have "\<exists>k::nat. x < ereal (real k)" |
2372 |
2345 |
2373 abbreviation "liminf \<equiv> Liminf sequentially" |
2346 abbreviation "liminf \<equiv> Liminf sequentially" |
2374 |
2347 |
2375 abbreviation "limsup \<equiv> Limsup sequentially" |
2348 abbreviation "limsup \<equiv> Limsup sequentially" |
2376 |
2349 |
2377 lemma (in complete_lattice) less_INFD: |
|
2378 assumes "y < INFI A f"" i \<in> A" shows "y < f i" |
|
2379 proof - |
|
2380 note `y < INFI A f` |
|
2381 also have "INFI A f \<le> f i" using `i \<in> A` by (rule INF_leI) |
|
2382 finally show "y < f i" . |
|
2383 qed |
|
2384 |
|
2385 lemma liminf_SUPR_INFI: |
2350 lemma liminf_SUPR_INFI: |
2386 fixes f :: "nat \<Rightarrow> ereal" |
2351 fixes f :: "nat \<Rightarrow> ereal" |
2387 shows "liminf f = (SUP n. INF m:{n..}. f m)" |
2352 shows "liminf f = (SUP n. INF m:{n..}. f m)" |
2388 unfolding Liminf_Sup eventually_sequentially |
2353 unfolding Liminf_Sup eventually_sequentially |
2389 proof (safe intro!: antisym complete_lattice_class.Sup_least) |
2354 proof (safe intro!: antisym complete_lattice_class.Sup_least) |