equal
deleted
inserted
replaced
822 |
822 |
823 lemma tendsto_power [tendsto_intros]: "(f \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. f x ^ n) \<longlongrightarrow> a ^ n) F" |
823 lemma tendsto_power [tendsto_intros]: "(f \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. f x ^ n) \<longlongrightarrow> a ^ n) F" |
824 for f :: "'a \<Rightarrow> 'b::{power,real_normed_algebra}" |
824 for f :: "'a \<Rightarrow> 'b::{power,real_normed_algebra}" |
825 by (induct n) (simp_all add: tendsto_mult) |
825 by (induct n) (simp_all add: tendsto_mult) |
826 |
826 |
|
827 lemma tendsto_null_power: "\<lbrakk>(f \<longlongrightarrow> 0) F; 0 < n\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x ^ n) \<longlongrightarrow> 0) F" |
|
828 for f :: "'a \<Rightarrow> 'b::{power,real_normed_algebra_1}" |
|
829 using tendsto_power [of f 0 F n] by (simp add: power_0_left) |
|
830 |
827 lemma continuous_power [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. (f x)^n)" |
831 lemma continuous_power [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. (f x)^n)" |
828 for f :: "'a::t2_space \<Rightarrow> 'b::{power,real_normed_algebra}" |
832 for f :: "'a::t2_space \<Rightarrow> 'b::{power,real_normed_algebra}" |
829 unfolding continuous_def by (rule tendsto_power) |
833 unfolding continuous_def by (rule tendsto_power) |
830 |
834 |
831 lemma continuous_on_power [continuous_intros]: |
835 lemma continuous_on_power [continuous_intros]: |