src/HOL/Limits.thy
changeset 44568 e6f291cb5810
parent 44342 8321948340ea
child 44571 bd91b77c4cd6
     1.1 --- a/src/HOL/Limits.thy	Sat Aug 27 17:26:14 2011 +0200
     1.2 +++ b/src/HOL/Limits.thy	Sun Aug 28 09:20:12 2011 -0700
     1.3 @@ -791,6 +791,15 @@
     1.4  lemmas tendsto_mult [tendsto_intros] =
     1.5    bounded_bilinear.tendsto [OF bounded_bilinear_mult]
     1.6  
     1.7 +lemmas tendsto_mult_zero =
     1.8 +  bounded_bilinear.tendsto_zero [OF bounded_bilinear_mult]
     1.9 +
    1.10 +lemmas tendsto_mult_left_zero =
    1.11 +  bounded_bilinear.tendsto_left_zero [OF bounded_bilinear_mult]
    1.12 +
    1.13 +lemmas tendsto_mult_right_zero =
    1.14 +  bounded_bilinear.tendsto_right_zero [OF bounded_bilinear_mult]
    1.15 +
    1.16  lemma tendsto_power [tendsto_intros]:
    1.17    fixes f :: "'a \<Rightarrow> 'b::{power,real_normed_algebra}"
    1.18    shows "(f ---> a) F \<Longrightarrow> ((\<lambda>x. f x ^ n) ---> a ^ n) F"