src/HOL/Library/Liminf_Limsup.thy

   shows "\<not> trivial_limit F \<Longrightarrow> (f \<longlongrightarrow> f0) F \<longleftrightarrow> (Liminf F f = f0 \<and> Limsup F f = f0)"
   by (metis Liminf_eq_Limsup lim_imp_Limsup lim_imp_Liminf)
 
 lemma liminf_subseq_mono:
   fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
-  assumes "subseq r"
+  assumes "strict_mono r"
   shows "liminf X \<le> liminf (X \<circ> r) "
 proof-
   have "\<And>n. (INF m:{n..}. X m) \<le> (INF m:{n..}. (X \<circ> r) m)"
   proof (safe intro!: INF_mono)
     fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. X ma \<le> (X \<circ> r) m"
-      using seq_suble[OF \<open>subseq r\<close>, of m] by (intro bexI[of _ "r m"]) auto
+      using seq_suble[OF \<open>strict_mono r\<close>, of m] by (intro bexI[of _ "r m"]) auto
   qed
   then show ?thesis by (auto intro!: SUP_mono simp: liminf_SUP_INF comp_def)
 qed
 
 lemma limsup_subseq_mono:
   fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
-  assumes "subseq r"
+  assumes "strict_mono r"
   shows "limsup (X \<circ> r) \<le> limsup X"
 proof-
   have "(SUP m:{n..}. (X \<circ> r) m) \<le> (SUP m:{n..}. X m)" for n
   proof (safe intro!: SUP_mono)
     fix m :: nat
     assume "n \<le> m"
     then show "\<exists>ma\<in>{n..}. (X \<circ> r) m \<le> X ma"
-      using seq_suble[OF \<open>subseq r\<close>, of m] by (intro bexI[of _ "r m"]) auto
+      using seq_suble[OF \<open>strict_mono r\<close>, of m] by (intro bexI[of _ "r m"]) auto
   qed
   then show ?thesis
     by (auto intro!: INF_mono simp: limsup_INF_SUP comp_def)
 qed
 

        (auto simp: INF_lower eventually_sequentially INF_less_iff intro: le_less_trans)
 qed
 
 lemma compact_complete_linorder:
   fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
-  shows "\<exists>l r. subseq r \<and> (X \<circ> r) \<longlonglongrightarrow> l"
-proof -
-  obtain r where "subseq r" and mono: "monoseq (X \<circ> r)"
+  shows "\<exists>l r. strict_mono r \<and> (X \<circ> r) \<longlonglongrightarrow> l"
+proof -
+  obtain r where "strict_mono r" and mono: "monoseq (X \<circ> r)"
     using seq_monosub[of X]
     unfolding comp_def
     by auto
   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)"
     by (auto simp add: monoseq_def)
   then obtain l where "(X \<circ> r) \<longlonglongrightarrow> l"
      using lim_increasing_cl[of "X \<circ> r"] lim_decreasing_cl[of "X \<circ> r"]
      by auto
   then show ?thesis
-    using \<open>subseq r\<close> by auto
+    using \<open>strict_mono r\<close> by auto
 qed
 
 lemma tendsto_Limsup:
   fixes f :: "_ \<Rightarrow> 'a :: {complete_linorder,linorder_topology}"
   shows "F \<noteq> bot \<Longrightarrow> Limsup F f = Liminf F f \<Longrightarrow> (f \<longlongrightarrow> Limsup F f) F"