src/HOL/Limits.thy
changeset 60182 e1ea5a6379c9
parent 60141 833adf7db7d8
child 60721 c1b7793c23a3
     1.1 --- a/src/HOL/Limits.thy	Wed May 06 15:04:38 2015 +0200
     1.2 +++ b/src/HOL/Limits.thy	Thu May 07 15:34:28 2015 +0200
     1.3 @@ -1183,6 +1183,12 @@
     1.4    using filterlim_tendsto_pos_mult_at_top[OF assms(1,2), of "\<lambda>x. - g x"] assms(3)
     1.5    unfolding filterlim_uminus_at_bot by simp
     1.6  
     1.7 +lemma filterlim_tendsto_neg_mult_at_bot:
     1.8 +  assumes c: "(f ---> c) F" "(c::real) < 0" and g: "filterlim g at_top F"
     1.9 +  shows "LIM x F. f x * g x :> at_bot"
    1.10 +  using c filterlim_tendsto_pos_mult_at_top[of "\<lambda>x. - f x" "- c" F, OF _ _ g]
    1.11 +  unfolding filterlim_uminus_at_bot tendsto_minus_cancel_left by simp
    1.12 +
    1.13  lemma filterlim_pow_at_top:
    1.14    fixes f :: "real \<Rightarrow> real"
    1.15    assumes "0 < n" and f: "LIM x F. f x :> at_top"