src/HOL/Limits.thy
changeset 64394 141e1ed8d5a0
parent 64287 d85d88722745
child 65036 ab7e11730ad8
     1.1 --- a/src/HOL/Limits.thy	Tue Oct 25 11:55:38 2016 +0200
     1.2 +++ b/src/HOL/Limits.thy	Tue Oct 25 15:46:07 2016 +0100
     1.3 @@ -1367,7 +1367,7 @@
     1.4  
     1.5  lemma tendsto_mult_filterlim_at_infinity:
     1.6    fixes c :: "'a::real_normed_field"
     1.7 -  assumes "F \<noteq> bot" "(f \<longlongrightarrow> c) F" "c \<noteq> 0"
     1.8 +  assumes  "(f \<longlongrightarrow> c) F" "c \<noteq> 0"
     1.9    assumes "filterlim g at_infinity F"
    1.10    shows "filterlim (\<lambda>x. f x * g x) at_infinity F"
    1.11  proof -
    1.12 @@ -1379,7 +1379,7 @@
    1.13      by (auto intro: filterlim_at_infinity_imp_eventually_ne tendsto_imp_eventually_ne eventually_conj)
    1.14    then show ?thesis
    1.15      by (subst filterlim_inverse_at_iff[symmetric]) simp_all
    1.16 -qed
    1.17 +qed  
    1.18  
    1.19  lemma tendsto_inverse_0_at_top: "LIM x F. f x :> at_top \<Longrightarrow> ((\<lambda>x. inverse (f x) :: real) \<longlongrightarrow> 0) F"
    1.20   by (metis filterlim_at filterlim_mono[OF _ at_top_le_at_infinity order_refl] filterlim_inverse_at_iff)