src/HOL/Library/Liminf_Limsup.thy
changeset 66447 a1f5c5c26fa6
parent 63895 9afa979137da
child 68860 f443ec10447d
     1.1 --- a/src/HOL/Library/Liminf_Limsup.thy	Thu Aug 17 14:40:42 2017 +0200
     1.2 +++ b/src/HOL/Library/Liminf_Limsup.thy	Thu Aug 17 14:52:56 2017 +0200
     1.3 @@ -379,20 +379,20 @@
     1.4  
     1.5  lemma liminf_subseq_mono:
     1.6    fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
     1.7 -  assumes "subseq r"
     1.8 +  assumes "strict_mono r"
     1.9    shows "liminf X \<le> liminf (X \<circ> r) "
    1.10  proof-
    1.11    have "\<And>n. (INF m:{n..}. X m) \<le> (INF m:{n..}. (X \<circ> r) m)"
    1.12    proof (safe intro!: INF_mono)
    1.13      fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. X ma \<le> (X \<circ> r) m"
    1.14 -      using seq_suble[OF \<open>subseq r\<close>, of m] by (intro bexI[of _ "r m"]) auto
    1.15 +      using seq_suble[OF \<open>strict_mono r\<close>, of m] by (intro bexI[of _ "r m"]) auto
    1.16    qed
    1.17    then show ?thesis by (auto intro!: SUP_mono simp: liminf_SUP_INF comp_def)
    1.18  qed
    1.19  
    1.20  lemma limsup_subseq_mono:
    1.21    fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
    1.22 -  assumes "subseq r"
    1.23 +  assumes "strict_mono r"
    1.24    shows "limsup (X \<circ> r) \<le> limsup X"
    1.25  proof-
    1.26    have "(SUP m:{n..}. (X \<circ> r) m) \<le> (SUP m:{n..}. X m)" for n
    1.27 @@ -400,7 +400,7 @@
    1.28      fix m :: nat
    1.29      assume "n \<le> m"
    1.30      then show "\<exists>ma\<in>{n..}. (X \<circ> r) m \<le> X ma"
    1.31 -      using seq_suble[OF \<open>subseq r\<close>, of m] by (intro bexI[of _ "r m"]) auto
    1.32 +      using seq_suble[OF \<open>strict_mono r\<close>, of m] by (intro bexI[of _ "r m"]) auto
    1.33    qed
    1.34    then show ?thesis
    1.35      by (auto intro!: INF_mono simp: limsup_INF_SUP comp_def)
    1.36 @@ -587,9 +587,9 @@
    1.37  
    1.38  lemma compact_complete_linorder:
    1.39    fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
    1.40 -  shows "\<exists>l r. subseq r \<and> (X \<circ> r) \<longlonglongrightarrow> l"
    1.41 +  shows "\<exists>l r. strict_mono r \<and> (X \<circ> r) \<longlonglongrightarrow> l"
    1.42  proof -
    1.43 -  obtain r where "subseq r" and mono: "monoseq (X \<circ> r)"
    1.44 +  obtain r where "strict_mono r" and mono: "monoseq (X \<circ> r)"
    1.45      using seq_monosub[of X]
    1.46      unfolding comp_def
    1.47      by auto
    1.48 @@ -599,7 +599,7 @@
    1.49       using lim_increasing_cl[of "X \<circ> r"] lim_decreasing_cl[of "X \<circ> r"]
    1.50       by auto
    1.51    then show ?thesis
    1.52 -    using \<open>subseq r\<close> by auto
    1.53 +    using \<open>strict_mono r\<close> by auto
    1.54  qed
    1.55  
    1.56  lemma tendsto_Limsup: