src/HOL/Real_Vector_Spaces.thy

 
 lemma metric_LIMSEQ_D: "X \<longlonglongrightarrow> L \<Longrightarrow> 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r"
   for L :: "'a::metric_space"
   by (simp add: lim_sequentially)
 
+lemma LIMSEQ_norm_0:
+  assumes  "\<And>n::nat. norm (f n) < 1 / real (Suc n)"
+  shows "f \<longlonglongrightarrow> 0"
+proof (rule metric_LIMSEQ_I)
+  fix \<epsilon> :: "real"
+  assume "\<epsilon> > 0"
+  then obtain N::nat where "\<epsilon> > inverse N" "N > 0"
+    by (metis neq0_conv real_arch_inverse)
+  then have "norm (f n) < \<epsilon>" if "n \<ge> N" for n
+  proof -
+    have "1 / (Suc n) \<le> 1 / N"
+      using \<open>0 < N\<close> inverse_of_nat_le le_SucI that by blast
+    also have "\<dots> < \<epsilon>"
+      by (metis (no_types) \<open>inverse (real N) < \<epsilon>\<close> inverse_eq_divide)
+    finally show ?thesis
+      by (meson assms less_eq_real_def not_le order_trans)
+  qed
+  then show "\<exists>no. \<forall>n\<ge>no. dist (f n) 0 < \<epsilon>"
+    by auto
+qed
+
 
 subsubsection \<open>Limits of Functions\<close>
 
 lemma LIM_def: "f \<midarrow>a\<rightarrow> L \<longleftrightarrow> (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r)"
   for a :: "'a::metric_space" and L :: "'b::metric_space"