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: