--- a/src/HOL/Library/Landau_Symbols.thy Thu Feb 16 10:42:39 2023 +0000
+++ b/src/HOL/Library/Landau_Symbols.thy Thu Feb 16 12:21:21 2023 +0000
@@ -1742,6 +1742,10 @@
by (rule Lim_transform_eventually)
qed (simp_all add: asymp_equiv_def)
+lemma tendsto_imp_asymp_equiv_const:
+ assumes "(f \<longlongrightarrow> c) F" "c \<noteq> 0"
+ shows "f \<sim>[F] (\<lambda>_. c)"
+ by (rule asymp_equivI' tendsto_eq_intros assms refl)+ (use assms in auto)
lemma asymp_equiv_cong:
assumes "eventually (\<lambda>x. f1 x = f2 x) F" "eventually (\<lambda>x. g1 x = g2 x) F"