src/HOL/Library/Landau_Symbols.thy

 qed
 
 
 subsection \<open>Asymptotic Equivalence\<close>
 
-(* TODO Move *)
-lemma tendsto_eventually: "eventually (\<lambda>x. f x = c) F \<Longrightarrow> filterlim f (nhds c) F"
-  by (simp add: eventually_mono eventually_nhds_x_imp_x filterlim_iff)
-
 named_theorems asymp_equiv_intros
 named_theorems asymp_equiv_simps
 
 definition asymp_equiv :: "('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> 'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
   (\<open>_ \<sim>[_] _\<close> [51, 10, 51] 50)

 proof (intro asymp_equivI)
   have "eventually (\<lambda>x. 1 = (if f x = 0 \<and> f x = 0 then 1 else f x / f x)) F"
     by (intro always_eventually) simp
   moreover have "((\<lambda>_. 1) \<longlongrightarrow> 1) F" by simp
   ultimately show "((\<lambda>x. if f x = 0 \<and> f x = 0 then 1 else f x / f x) \<longlongrightarrow> 1) F"
-    by (simp add: Landau_Symbols.tendsto_eventually)
+    by (simp add: tendsto_eventually)
 qed
 
 lemma asymp_equiv_symI: 
   assumes "f \<sim>[F] g"
   shows   "g \<sim>[F] f"