src/HOL/Limits.thy
changeset 65680 378a2f11bec9
parent 65578 e4997c181cce
child 66447 a1f5c5c26fa6
     1.1 --- a/src/HOL/Limits.thy	Tue May 02 10:25:27 2017 +0200
     1.2 +++ b/src/HOL/Limits.thy	Tue May 02 14:34:06 2017 +0100
     1.3 @@ -824,6 +824,10 @@
     1.4    for f :: "'a \<Rightarrow> 'b::{power,real_normed_algebra}"
     1.5    by (induct n) (simp_all add: tendsto_mult)
     1.6  
     1.7 +lemma tendsto_null_power: "\<lbrakk>(f \<longlongrightarrow> 0) F; 0 < n\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x ^ n) \<longlongrightarrow> 0) F"
     1.8 +    for f :: "'a \<Rightarrow> 'b::{power,real_normed_algebra_1}"
     1.9 +  using tendsto_power [of f 0 F n] by (simp add: power_0_left)
    1.10 +
    1.11  lemma continuous_power [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. (f x)^n)"
    1.12    for f :: "'a::t2_space \<Rightarrow> 'b::{power,real_normed_algebra}"
    1.13    unfolding continuous_def by (rule tendsto_power)