equal
deleted
inserted
replaced
789 bounded_bilinear.tendsto [OF bounded_bilinear_scaleR] |
789 bounded_bilinear.tendsto [OF bounded_bilinear_scaleR] |
790 |
790 |
791 lemmas tendsto_mult [tendsto_intros] = |
791 lemmas tendsto_mult [tendsto_intros] = |
792 bounded_bilinear.tendsto [OF bounded_bilinear_mult] |
792 bounded_bilinear.tendsto [OF bounded_bilinear_mult] |
793 |
793 |
|
794 lemmas tendsto_mult_zero = |
|
795 bounded_bilinear.tendsto_zero [OF bounded_bilinear_mult] |
|
796 |
|
797 lemmas tendsto_mult_left_zero = |
|
798 bounded_bilinear.tendsto_left_zero [OF bounded_bilinear_mult] |
|
799 |
|
800 lemmas tendsto_mult_right_zero = |
|
801 bounded_bilinear.tendsto_right_zero [OF bounded_bilinear_mult] |
|
802 |
794 lemma tendsto_power [tendsto_intros]: |
803 lemma tendsto_power [tendsto_intros]: |
795 fixes f :: "'a \<Rightarrow> 'b::{power,real_normed_algebra}" |
804 fixes f :: "'a \<Rightarrow> 'b::{power,real_normed_algebra}" |
796 shows "(f ---> a) F \<Longrightarrow> ((\<lambda>x. f x ^ n) ---> a ^ n) F" |
805 shows "(f ---> a) F \<Longrightarrow> ((\<lambda>x. f x ^ n) ---> a ^ n) F" |
797 by (induct n) (simp_all add: tendsto_const tendsto_mult) |
806 by (induct n) (simp_all add: tendsto_const tendsto_mult) |
798 |
807 |