src/HOL/Limits.thy
 changeset 65578 e4997c181cce parent 65204 d23eded35a33 child 65680 378a2f11bec9
```     1.1 --- a/src/HOL/Limits.thy	Tue Apr 25 08:38:23 2017 +0200
1.2 +++ b/src/HOL/Limits.thy	Tue Apr 25 16:39:54 2017 +0100
1.3 @@ -1799,10 +1799,12 @@
1.4    using assms by simp
1.5
1.6  text \<open>An unbounded sequence's inverse tends to 0.\<close>
1.7 -lemma LIMSEQ_inverse_zero: "\<forall>r::real. \<exists>N. \<forall>n\<ge>N. r < X n \<Longrightarrow> (\<lambda>n. inverse (X n)) \<longlonglongrightarrow> 0"
1.8 +lemma LIMSEQ_inverse_zero:
1.9 +  assumes "\<And>r::real. \<exists>N. \<forall>n\<ge>N. r < X n"
1.10 +  shows "(\<lambda>n. inverse (X n)) \<longlonglongrightarrow> 0"
1.11    apply (rule filterlim_compose[OF tendsto_inverse_0])
1.12    apply (simp add: filterlim_at_infinity[OF order_refl] eventually_sequentially)
1.13 -  apply (metis abs_le_D1 linorder_le_cases linorder_not_le)
1.14 +  apply (metis assms abs_le_D1 linorder_le_cases linorder_not_le)
1.15    done
1.16
1.17  text \<open>The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity.\<close>
1.18 @@ -2189,16 +2191,16 @@
1.19    using LIM_offset_zero_cancel[of f a L] LIM_offset_zero[of f L a] by auto
1.20
1.21  lemma LIM_zero: "(f \<longlongrightarrow> l) F \<Longrightarrow> ((\<lambda>x. f x - l) \<longlongrightarrow> 0) F"
1.22 -  for f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
1.23 +  for f :: "'a \<Rightarrow> 'b::real_normed_vector"
1.24    unfolding tendsto_iff dist_norm by simp
1.25
1.26  lemma LIM_zero_cancel:
1.27 -  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
1.28 +  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
1.29    shows "((\<lambda>x. f x - l) \<longlongrightarrow> 0) F \<Longrightarrow> (f \<longlongrightarrow> l) F"
1.30  unfolding tendsto_iff dist_norm by simp
1.31
1.32  lemma LIM_zero_iff: "((\<lambda>x. f x - l) \<longlongrightarrow> 0) F = (f \<longlongrightarrow> l) F"
1.33 -  for f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
1.34 +  for f :: "'a \<Rightarrow> 'b::real_normed_vector"
1.35    unfolding tendsto_iff dist_norm by simp
1.36
1.37  lemma LIM_imp_LIM:
```