diff -r 0a12ca4f3e8d -r 26171a89466a src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Sat Jun 26 20:55:43 2021 +0200
+++ b/src/HOL/Limits.thy	Mon Jun 28 15:05:46 2021 +0100
@@ -1777,7 +1777,15 @@
 qed
 
 lemma tendsto_inverse_0_at_top: "LIM x F. f x :> at_top \<Longrightarrow> ((\<lambda>x. inverse (f x) :: real) \<longlongrightarrow> 0) F"
- by (metis filterlim_at filterlim_mono[OF _ at_top_le_at_infinity order_refl] filterlim_inverse_at_iff)
+  by (metis filterlim_at filterlim_mono[OF _ at_top_le_at_infinity order_refl] filterlim_inverse_at_iff)
+
+lemma filterlim_inverse_at_top_iff:
+  "eventually (\<lambda>x. 0 < f x) F \<Longrightarrow> (LIM x F. inverse (f x) :> at_top) \<longleftrightarrow> (f \<longlongrightarrow> (0 :: real)) F"
+  by (auto dest: tendsto_inverse_0_at_top filterlim_inverse_at_top)
+
+lemma filterlim_at_top_iff_inverse_0:
+  "eventually (\<lambda>x. 0 < f x) F \<Longrightarrow> (LIM x F. f x :> at_top) \<longleftrightarrow> ((inverse \<circ> f) \<longlongrightarrow> (0 :: real)) F"
+  using filterlim_inverse_at_top_iff [of "inverse \<circ> f"] by auto
 
 lemma real_tendsto_divide_at_top:
   fixes c::"real"