349 by (intro SUP_cong refl continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]]) |
349 by (intro SUP_cong refl continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]]) |
350 (auto dest!: eventually_happens simp: F) |
350 (auto dest!: eventually_happens simp: F) |
351 finally show ?thesis |
351 finally show ?thesis |
352 by (auto simp: Liminf_def) |
352 by (auto simp: Liminf_def) |
353 qed |
353 qed |
|
354 subsection \<open>More Limits\<close> |
|
355 |
|
356 lemma convergent_limsup_cl: |
|
357 fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}" |
|
358 shows "convergent X \<Longrightarrow> limsup X = lim X" |
|
359 by (auto simp: convergent_def limI lim_imp_Limsup) |
|
360 |
|
361 lemma convergent_liminf_cl: |
|
362 fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}" |
|
363 shows "convergent X \<Longrightarrow> liminf X = lim X" |
|
364 by (auto simp: convergent_def limI lim_imp_Liminf) |
|
365 |
|
366 lemma lim_increasing_cl: |
|
367 assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<ge> f m" |
|
368 obtains l where "f ----> (l::'a::{complete_linorder,linorder_topology})" |
|
369 proof |
|
370 show "f ----> (SUP n. f n)" |
|
371 using assms |
|
372 by (intro increasing_tendsto) |
|
373 (auto simp: SUP_upper eventually_sequentially less_SUP_iff intro: less_le_trans) |
|
374 qed |
|
375 |
|
376 lemma lim_decreasing_cl: |
|
377 assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<le> f m" |
|
378 obtains l where "f ----> (l::'a::{complete_linorder,linorder_topology})" |
|
379 proof |
|
380 show "f ----> (INF n. f n)" |
|
381 using assms |
|
382 by (intro decreasing_tendsto) |
|
383 (auto simp: INF_lower eventually_sequentially INF_less_iff intro: le_less_trans) |
|
384 qed |
|
385 |
|
386 lemma compact_complete_linorder: |
|
387 fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}" |
|
388 shows "\<exists>l r. subseq r \<and> (X \<circ> r) ----> l" |
|
389 proof - |
|
390 obtain r where "subseq r" and mono: "monoseq (X \<circ> r)" |
|
391 using seq_monosub[of X] |
|
392 unfolding comp_def |
|
393 by auto |
|
394 then have "(\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) m \<le> (X \<circ> r) n) \<or> (\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) n \<le> (X \<circ> r) m)" |
|
395 by (auto simp add: monoseq_def) |
|
396 then obtain l where "(X \<circ> r) ----> l" |
|
397 using lim_increasing_cl[of "X \<circ> r"] lim_decreasing_cl[of "X \<circ> r"] |
|
398 by auto |
|
399 then show ?thesis |
|
400 using \<open>subseq r\<close> by auto |
|
401 qed |
354 |
402 |
355 end |
403 end |