equal
deleted
inserted
replaced
283 using assms apply auto |
283 using assms apply auto |
284 done |
284 done |
285 finally show ?thesis . |
285 finally show ?thesis . |
286 qed |
286 qed |
287 |
287 |
|
288 lemma tendsto_powr [tendsto_intros]: |
|
289 "\<lbrakk>(f ---> a) F; (g ---> b) F; 0 < a\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x powr g x) ---> a powr b) F" |
|
290 unfolding powr_def by (intro tendsto_intros) |
|
291 |
288 (* FIXME: generalize by replacing d by with g x and g ---> d? *) |
292 (* FIXME: generalize by replacing d by with g x and g ---> d? *) |
289 lemma tendsto_zero_powrI: |
293 lemma tendsto_zero_powrI: |
290 assumes "eventually (\<lambda>x. 0 < f x ) F" and "(f ---> 0) F" |
294 assumes "eventually (\<lambda>x. 0 < f x ) F" and "(f ---> 0) F" |
291 assumes "0 < d" |
295 assumes "0 < d" |
292 shows "((\<lambda>x. f x powr d) ---> 0) F" |
296 shows "((\<lambda>x. f x powr d) ---> 0) F" |