src/HOL/Limits.thy
changeset 66793 deabce3ccf1f
parent 66456 621897f47fab
child 66827 c94531b5007d
     1.1 --- a/src/HOL/Limits.thy	Sun Oct 08 16:50:37 2017 +0200
     1.2 +++ b/src/HOL/Limits.thy	Mon Oct 09 15:34:23 2017 +0100
     1.3 @@ -820,6 +820,11 @@
     1.4  lemmas tendsto_mult_right_zero =
     1.5    bounded_bilinear.tendsto_right_zero [OF bounded_bilinear_mult]
     1.6  
     1.7 +lemma tendsto_divide_zero:
     1.8 +  fixes c :: "'a::real_normed_field"
     1.9 +  shows "(f \<longlongrightarrow> 0) F \<Longrightarrow> ((\<lambda>x. f x / c) \<longlongrightarrow> 0) F"
    1.10 +  by (cases "c=0") (simp_all add: divide_inverse tendsto_mult_left_zero)
    1.11 +
    1.12  lemma tendsto_power [tendsto_intros]: "(f \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. f x ^ n) \<longlongrightarrow> a ^ n) F"
    1.13    for f :: "'a \<Rightarrow> 'b::{power,real_normed_algebra}"
    1.14    by (induct n) (simp_all add: tendsto_mult)