src/HOL/Topological_Spaces.thy

     by (auto simp: choice_iff)
   then show ?thesis
     by (auto intro!: exI[of _ "\<lambda>n. r (((Suc \<circ> r) ^^ Suc n) 0)"]
              simp: less_eq_Suc_le strict_mono_Suc_iff)
 qed
+
+lemma sequentially_offset: 
+  assumes "eventually (\<lambda>i. P i) sequentially"
+  shows "eventually (\<lambda>i. P (i + k)) sequentially"
+  using assms by (rule eventually_sequentially_seg [THEN iffD2])
+
+lemma seq_offset_neg: 
+  "(f \<longlongrightarrow> l) sequentially \<Longrightarrow> ((\<lambda>i. f(i - k)) \<longlongrightarrow> l) sequentially"
+  apply (erule filterlim_compose)
+  apply (simp add: filterlim_def le_sequentially eventually_filtermap eventually_sequentially, arith)
+  done
 
 lemma filterlim_subseq: "strict_mono f \<Longrightarrow> filterlim f sequentially sequentially"
   unfolding filterlim_iff by (metis eventually_subseq)
 
 lemma strict_mono_o: "strict_mono r \<Longrightarrow> strict_mono s \<Longrightarrow> strict_mono (r \<circ> s)"

   by (auto intro: continuous_at_imp_continuous_at_within simp: continuous_on_eq_continuous_within)
 
 lemma isCont_o2: "isCont f a \<Longrightarrow> isCont g (f a) \<Longrightarrow> isCont (\<lambda>x. g (f x)) a"
   unfolding isCont_def by (rule tendsto_compose)
 
-lemma isCont_o[continuous_intros]: "isCont f a \<Longrightarrow> isCont g (f a) \<Longrightarrow> isCont (g \<circ> f) a"
+lemma continuous_at_compose[continuous_intros]: "isCont f a \<Longrightarrow> isCont g (f a) \<Longrightarrow> isCont (g \<circ> f) a"
   unfolding o_def by (rule isCont_o2)
 
 lemma isCont_tendsto_compose: "isCont g l \<Longrightarrow> (f \<longlongrightarrow> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) \<longlongrightarrow> g l) F"
   unfolding isCont_def by (rule tendsto_compose)