equal
deleted
inserted
replaced
375 by (rule tendsto) |
375 by (rule tendsto) |
376 |
376 |
377 lemma LIMSEQ_mult: |
377 lemma LIMSEQ_mult: |
378 fixes a b :: "'a::real_normed_algebra" |
378 fixes a b :: "'a::real_normed_algebra" |
379 shows "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b" |
379 shows "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b" |
380 by (rule mult.tendsto) |
380 by (rule tendsto_mult) |
381 |
381 |
382 lemma increasing_LIMSEQ: |
382 lemma increasing_LIMSEQ: |
383 fixes f :: "nat \<Rightarrow> real" |
383 fixes f :: "nat \<Rightarrow> real" |
384 assumes inc: "!!n. f n \<le> f (Suc n)" |
384 assumes inc: "!!n. f n \<le> f (Suc n)" |
385 and bdd: "!!n. f n \<le> l" |
385 and bdd: "!!n. f n \<le> l" |